Lightnews — Scholar-powered news

Rado Kirov

@radokirov.bsky.social

62 followers 28 following 79 posts

engineering at stripe. recovering academic.

Posts Media Videos Starter Packs

Rado Kirov @radokirov.bsky.social · 11d

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.

Rado Kirov @radokirov.bsky.social · 14d

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.

Rado Kirov @radokirov.bsky.social · 14d

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.

Rado Kirov @radokirov.bsky.social · 15d

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

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

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...

docs.google.com

Rado Kirov @radokirov.bsky.social · 15d

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)

Rado Kirov @radokirov.bsky.social · 16d

Er reals

Rado Kirov @radokirov.bsky.social · 16d

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

Rado Kirov @radokirov.bsky.social · 16d

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.

Rado Kirov @radokirov.bsky.social · 16d

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

Rado Kirov @radokirov.bsky.social · 16d

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.

Rado Kirov @radokirov.bsky.social · 16d

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.

Rado Kirov @radokirov.bsky.social · 17d

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

Learning Lean: Part 4

It’s been 3 months since my previous post about learning Lean part 3, so it’s time to write another one. I have mostly continued to work through Tao’s Analysis book through his excellent companion - w...

rkirov.github.io

Rado Kirov @radokirov.bsky.social · 21d

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.

Rado Kirov @radokirov.bsky.social · 21d

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.

Rado Kirov @radokirov.bsky.social · 21d

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

Rado Kirov @radokirov.bsky.social · 21d

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

Rado Kirov @radokirov.bsky.social · 21d

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.

Rado Kirov @radokirov.bsky.social · 22d

Did you slay the chapter 3 boss?

Rado Kirov @radokirov.bsky.social · Sep 8

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 :)

Rado Kirov @radokirov.bsky.social · Sep 8

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)

Rado Kirov @radokirov.bsky.social · Sep 8

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.

Combinatorial proof - Wikipedia

en.m.wikipedia.org

Rado Kirov @radokirov.bsky.social · Sep 8

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.

Rado Kirov @radokirov.bsky.social · Sep 8

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

Rado Kirov @radokirov.bsky.social · Sep 6

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.

Rado Kirov @radokirov.bsky.social · Sep 6

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.