All of this should be equivalent to visualizing lambda calculus (by Curry-Howard), which opens to more visualizations/gamifications.

But which one would make the best mobile puzzle game?

[1] worrydream.com/AlligatorEggs/
[2] bntr.itch.io/visual-lambda
[3] github.com/prathyvsh/la...

Can wait to see a Fields medalist asking what’s the difference between common js and EcmaScript modules.

We got enough interest and are kicking this off this Monday 7:00pm at moxsf.com. Fill in the interest form if you would like to join us.

We got 11 sign-up so this might happen. One sign-up mistyped their email, and I couldn't reach them, so if you didn't get an email from me, please redo the form.

Next up, finding a venue.

I will consider it if I start to feel I need something that it can provide on top of my low tech tools, but also don’t want to involve more parties in this too prematurely.

Haven’t done this before, so I might be forgetting something, but only thing that comes to mind is needs a projector or a big screen.

course info - docs.google.com/document/d/1...

interest collection form - docs.google.com/forms/d/e/1F...

Er reals

Bad news - you have two more instances of this ahead, trichotomy of rationals and integers.

Yeah from my very limitted experience, they don’t really show up much when doing standard mathematics. Mostly lean getting stuck in dealing with universe polymorphism and one has to explicitly add universe parameters.

Do you plan to go into universes for the type system post?

But also where a new lean users needs most help due to the proliferation of tactics, with different powers and tradeoffs. So the first post would cover a lot of ground (also very dependent on the type of math one is trying to prove) but be more valuable long term.

One needs to understand the type system in order to prove anything so the second feels like a prerequisite for the first. Also from what I gather Lean types, while crazy fancy for people new to proof assistants, are a fairly standard construction. The extensibility model is where Lean shines.

On the (I hate Fins) part - I wonder if this proof in a set theory based assistant would look simper. Part of the problem is - Fins are whole types e.g. 3 in Fin 4 is very different from 3 in Fin 5. Tao suggested avoiding Fins by redefining Permutations as N -> N bijections that are id after n.

3) I am convinced this will be the only way to do math in 10-20 years, so fun to be part of the revolution as it is unfolding and maybe bring some experience from the software engineering world. These exercises are just a formal math proof version of the CS exercises we all did to learn programming.

My answer for why 1) it’s a fun puzzle, tickles my brain like The witness or Taiji but somehow it’s also a timeless classical axiomatic foundation of all mathematics 2) helps me restart my math knowledge journey (that I abandoned 15 years ago) hoping to connect to the FLT effort one day

It is obviously similar to well-structured software code, but also subtly different.

Thanks for the shoutout! Somehow I don’t have the patience to refactor my proofs once they check, so I enjoy reading your better structured solutions. While I am getting better at driving a proof through, it is still very unclear to me what a well-written proof looks like.