Rado Kirov

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.

Mathematics from Scratch in Lean Mathematics from Scratch with Lean In the 1890s, the world's top mathematicians embarked on an ambitious project: rebuild all of mathematics from scratch using pure logic. Today, you can join that sam...

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

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

Calling Bay Area math enthusiasts interested in weekly sessions doing rigorous foundational mathematics the modern way - with computer-verified proofs in Lean.

(An experiment in rigorous math education outside traditional academia)

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.

Newest installment in my journey of learning how to do math proofs with computers rkirov.github.io/posts/lean4/.

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.

Did you slay the chapter 3 boss?

Compare - f<T>(x: Arr<T>, y: T) to f {T: Type} (x: Arr T) (y: T). After lean I don’t want to write <> any more :)

The funny thing - languages with generics like TS already allow one very limited form of this - the generic param is implicit and can be inferred from arg types, but in dep typed languages types and values are treated uniformly, which has certain pleasing quality to it (but can be disorienting too)

You might then also enjoy many other combinotrial proofs for algebraic identities en.m.wikipedia.org/wiki/Combina... . Sum over k n choose k = 2^n using subsets is another classic.

Yeah, there is also macro expansion (I don’t fully understand if that is what in lean they call elaboration) that has to happen before (or together?) with typechecking.

I mean it does “run” just a bit earlier than usual :)

Don’t worry, you got it! There were parts of the proof that “rhymed” but I wasn’t experienced enough to refactor them. Judging by your other solutions you have gotten better than me at that, so I am looking forward to learning from your solution. Very curious how that improves perf too.

Yeah not automatically bottoming out on all definition first and then attempting to prove things was surprising to me. What was even more surprising was the few proofs where you have to intentionally transform a term in the opposite simp direction before you can apply some even more powerful lemma.

The duality is precisely swapping inputs and outputs in all arrows and recasting all object definitions in terms of arrows. It not surprising that things behave differently on both sides of ->, but they do come in pairs. The other one always behaves symmetrically. In your example consider Bottom.

Hand-wavy - there is a deep duality in all of logic / types - creating vs destroying information, True vs False, unit vs bottom type. Inputs vs outputs to a function are on different side of the duality, unlike the two argument to And or Or. The categorical view makes the duality most obvious.

Not sure if this counts as intuition or recasting the statement to the most abstract level possible, which can be either seen as a deep reason for this being true or too abstract and actually further from intuition.

If you want to looking the categorical things - look up initial and terminal objects and notice that they are same but with arrows reversed. Then observe that _ -> X is contravariant and X -> _ is covariant, i.e. they swap the directions of the arrows.

There are a bunch of categorical way of seeing this, but it only counts as intuition if you are steeped in that language (intuition is very dependent on your prior knowledge). Does the similar statement in logic True -> X is same as X but X -> True is True help?