lean

Bilingual

Are We Stuck with Lean?
2 months ago
- Three years ago, the author gave a talk suggesting that the mathematical community had a narrow window to choose a proof assistant, with Lean gaining momentum but not yet inevitable.
- The central question is whether any organization would seriously support an alternative to Lean, such as Metamath.
- Metamath offers two advantages: higher soundness assurance due to Metamath Zero, and a set-theoretic foundation that addresses concerns about the propositions-as-types philosophy.
- Lean's popularity may be driven by prominent figures rather than objective superiority; its main strength is the Mathlib library.
- AI's progress in formal mathematics makes it feasible to consider building analogous libraries for other provers, though quality remains a challenge.
- The author advocates for a viable alternative to Lean for the community's benefit, but this requires institutional support whose source is unclear.
Why Lean is faster than Rust
2 months ago
- Lean's DEFLATE implementation (lean-zip) outperforms pure Rust's miniz_oxide in both compression speed and ratio at most levels, e.g., 30% faster at level 6.
- The performance advantage is enabled by a formal proof of correctness (inflate_deflateRaw theorem), which allows AI agents to optimize the code autonomously without human review, ensuring no bugs are introduced.
- Pareto frontier graphs show lean-zip dominates miniz_oxide across all compression levels, and is competitive with optimized libraries like zlib-ng and zlib-rs at high levels.
- Caveats include higher memory consumption, slower decompression (1.45x slower), reliance on Lean's extern annotations for low-level functions, and that the proof only covers round-trip correctness, not side channels or performance.
- The experiment demonstrates that with formal verification, AI-driven optimization can make Lean competitive with fast languages for basic algorithms, but it is not a general claim that Lean is faster than Rust.
A Lean Syntax Primer — overreacted
2 months ago
- Lean uses `:=` for definitions and `=` for comparisons, with type inference for `String`, `Nat`, `Int`.
- `#eval` runs code and displays results in the InfoView, while `#print` can output to terminal.
- Proofs are written with `theorem` and tactics like `unfold`, `decide`, `simp`, and `omega`.
- Function calls use no parentheses or commas: `f a b c`; parentheses are only for grouping expressions.
- `let` bindings allow local definitions inside functions, and the last expression is the return value.
- Functions can be declared in multiple ways, with explicit or implicit types, including anonymous `fun` syntax.
- The universal quantifier `∀` enables proving statements for all possible values of a parameter.
- Implicit arguments `{ }` and instance arguments `[ ]` are automatically filled by Lean, reducing boilerplate.
- Lean is highly interactive: `Command+Click` on any identifier opens its definition or source.
The Math Is Haunted — overreacted
2 months ago
- Lean is a programming language used by mathematicians to formalize mathematics as code, enabling modularity and verification.
- The article demonstrates proving a simple theorem (2 = 2) using the `rfl` tactic, which closes goals of the form `x = x`.
- Introducing a false axiom (`math_is_haunted : 2 = 3`) allows proving contradictory statements, illustrating the importance of sound axioms.
- A proof checker only verifies logical conclusions from chosen axioms; if axioms are sound, proofs are sound, regardless of length.
- Efforts are ongoing to formalize Fermat's Last Theorem in Lean, a project expected to take many years.
- Resources for learning Lean include the Natural Numbers Game, Mathematics in Lean, and Tao's Analysis with a Lean companion.
Beyond Booleans — overreacted
2 months ago
- In Lean, logical statements like `2+2=4` are of type `Prop`, not Boolean.
- Propositions in Lean are also types; a proof is a value of that type.
- Proving a proposition is equivalent to constructing a value of its type.
- Multiple proofs of the same proposition are considered equal (proof irrelevance).
- Lean allows expressing constraints like 'x is between 0 and 1' as type-level proofs, enabling typed truthfulness.
- Proofs can be composed using existing theorems from Mathlib.
- The `Eq` type is defined with only one constructor `refl`, making it impossible to prove false equalities.
- This bridges mathematics and programming by computing logic, not just numbers.
We have proof automation now
2 months ago
- Dependently-typed languages like Lean offer powerful type systems but require significant proof effort, as seen in the seL4 project with 10x more proof code than implementation code.
- LLMs combined with proof irrelevance (the fact that only existence of proof matters) can automate proof generation, making dependent types more practical for everyday software engineering.
- Zstandard is a modern compression utility that uses Huffman and FSE (Finite State Entropy) coding; FSE achieves fractional bits per symbol by assigning multiple states to common symbols.
- Lean is a strict, purely functional language with mutation optimization (when reference count is 1) and support for imperative-style coding, making it suitable for performance-sensitive tasks.
- The author built a Zstandard decompressor in Lean and used LLMs to automatically prove properties of the FSE table construction, such as table size, state counts, and reachability of all states.
Introduction to Formal Verification with Lean Part 1
2 months ago
- Formal verification uses tools like Lean to write machine-checked proofs, ensuring mathematical correctness.
- This tutorial covers basic Lean concepts and verifies the One-Time Pad (OTP) protocol, a Shannon cipher.
- Learners define bitstrings as vectors over GF(2), prove XOR properties (commutativity, associativity, identity, self-inverse), and implement a Shannon cipher structure.
- The goal is to translate cryptographic definitions from Boneh & Shoup's textbook into Lean, culminating in proving OTP is a Shannon cipher.
- Lean is a functional programming language and theorem prover that automates proof tasks and supports collaboration.

Are We Stuck with Lean?

Why Lean is faster than Rust

A Lean Syntax Primer — overreacted

The Math Is Haunted — overreacted

Beyond Booleans — overreacted

We have proof automation now

Introduction to Formal Verification with Lean Part 1