Lean (proof assistant) Updated 2026-01-30
Source code:
- github.com/leanprover/lean4 why a separate repo per version... but it is what it is.
- github.com/leanprover/lean
The way Lean and Coq mix programming and mathematics is a thing of great beauty. This is especially notable in lean as you start to play with with things such as:
partialenv lean functions, and usingterminates_byto prove that certain functions terminate. Lean requires explicitly known if functions terminate or not to be able to use them in proofs.noncomputablefunctions. Lean allows you to define mathematical functions which you can't actually execute, and it tracks that explicitly
They are huge fans of Unicode characters! Check this out from a formal proof of the prime number theorem: github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/fbdbb5310d036d33b9797b35f3b04b08f2447a6e/PrimeNumberTheoremAnd/ZetaBounds.lean Here's map to Ascii: proofassistants.stackexchange.com/questions/954/does-lean-have-a-standard-ascii-representation/5289#5289
Their dependency graph thingy is just beautiful however: alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html
LinkedIn Updated 2025-07-16
Ciro Santilli's LinkedIn profile: www.linkedin.com/in/cirosantilli/ see also: accounts controlled by Ciro Accounts.
LinkedIn fully complies with censorship imposed locally by the Chinese government, and does so in a non-transparent way: cirosantilli.com/china-dictatorship/linkedin.
It is hard to understand what the point of that website is, as it is basically just a more closed version of Facebook, but alas, it has flourished as the only place where people post more useful content compared to Twitter and Facebook. In any case, Ciro just applies the same unfollow policy to all of them: aggressively filter your social media follows.
Microsoft Outlook Updated 2025-07-16