This page gathers Lean autoformalizations of results that are not from my articles, and texts sent to Hexagon, mainly written by AI. The Lean formalizations of my own papers are linked from the Publications and research page.

Lean formalizations

These formalizations are produced with these Claude Code skills, adapted from Scott Armstrong’s skills. Following the setup described in the post Autoformalization is now very easy, Claude Code acts as an orchestrator: it writes the Lean statements of the results, has them checked by an independent review, and freezes them once I have approved them. It then hands the proofs to worker agents running in parallel in the background (open models such as Kimi through Open Math OS for routine steps, and GPT models through Codex for the harder ones), while smaller Claude agents audit and clean up. A result is accepted only once it compiles, passes an axiom check and passes an independent audit.

• Random Trees in Lean (documentation)
  A Lean 4 library on random trees and the classical probability behind their scaling limits. It covers finite and locally finite Bienaymé–Galton–Watson trees and their Łukasiewicz coding, the Skorokhod space and weak convergence, the spectrally positive stable Lévy process with its excursion theory and height process, the Duquesne–Le Gall scaling limits of Bienaymé–Galton–Watson trees and forests, and the Gromov–Hausdorff–Prokhorov geometry of continuum trees. It is still in development (version 0.1.1), and every proof is checked by Lean’s kernel using only the standard axioms.

Hexagon

Texts sent to Hexagon, mainly written by AI.

Coming soon.