#lean #math #code4math

Can one then show that 1 = 2, say by manipulating a - (a + 1) = 0 into a = a + 1, adding 1 to both sides, and subtracting a? No! The reason why is that LEAN knows that subtraction in the naturals isn't subtractive. (Or rather it doesn't think that it is subtractive).

(3/3)

The proof in LEAN is very simple: tell it to use 0. What happens behind the scenes is that, in LEAN, 0 - 1 = 0 (when considered in natural numbers). I think this is because it's convenient to have naturals closed under basic operations.

(2/3)

At this morning's opening session of the code4math opening (preview.scholarlattice.org/collections/...), I learned that in LEAN one can prove the following theorem:

There exists a natural number a such that a - (a + 1) = 0.

(1/3)

+1 for Secret Mall Apartment

It definitely contributes to math-as-mysticism, incantations done by all-knowing mages that is intractable to mere mortals. But this is far from the truth! And we want more people to recognize that mathematical thinking is useful and approachable and worthwhile!

And also this was the source of bsky.app/profile/davi...

I wrote about this some here.

davidlowryduda.com/paper-fibona...

I just submitted "The Fibonacci Zeta Function and Continuation" (or as I think of it it, Fibonacci Zeta Function I) to the arxiv. Cheers to my collaborators Eran Assaf, Chan Kuan, and Alex Walker.

I feel like I've accomplished something, so I will goof off with my daughter for a while.

Pro tip for folks who use beamer: Turn off the nav symbols!
\setbeamertemplate{navigation symbols}{}

🧪⚛️🧮

Hey #MathSky! 👋 Interested in learning how to leverage #computing to advance your mathematics research and teaching? You may be interested in the @aimathematics.bsky.social sponsored "Leveraging GitHub and AI for Mathematics Research and Teaching" PEP: jointmathematicsmeetings.org/meetings/nat...

Thanks. I've never heard of Ologs before.

I'm very interested in the different notetaking systems that mathematicians, scientists, programmers, and engineers use. This is talked about somewhere, right?

I'm looking for more than "I use a notebook" or "I use [app name]". I want to know how people actually use and organize their notes.

This is the Fibonacci zeta function. Actually, it's the odd-indexed Fibonacci zeta function, but that's ok.

davidlowryduda.com/odd-fibonacci/

I appreciate the tip, thanks!

Hello, World!