List of proof assistants

Source code:

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

Their dependency graph thingy is just beautiful however: alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html

Their 2025 current installation method is bullshit, recommends VS Code extension on Ubuntu. Lol.

From CLI:Then when you run:it downloads the lean executable for you. Insane shit, could only come from a Microsoft mindset.

This tutorial has the merit of actually trying you to do some meaningful mathematics before teaching you a billion items of syntax and dependent type theory nuances.

Here is a specific minimal example of how to use mathlib4: proofassistants.stackexchange.com/questions/2526/how-to-run-lean4-with-mathlib-manually/5299#5299

This used to have the best name ever allowing you to say:to English speakers and watch their faces drop.

But in 2023 the bastards renamed it to "Rocq", presumably pronounced "rock". Why, God, why.

This will never work but OK. New custom language after Lean.

It seems to implement Zermelo-Fraenkel set theory.