Lean Focused Research Organization on Mythryl: “Recently came across @filiplajszczak.bsky.social's series…”

Recently came across @filiplajszczak.bsky.social's series formalizing a 1967 math textbook in #LeanLang. Designed for those "with no prior experience with formalization" - nice bridge for newcomers to #LeanProver! Read the intro post here: filip.lajszczak.dev/lean-4-with-...

filip.lajszczak.devLean 4 with a Math Textbook - Part 0 - Introduction — Some opinions, held with varying degrees of certainty.

10/9/25, 7:44 pm7 reposts10 likes

Post