Link identifier archive #link-archive-thumb-soap-11563
Venerdì 8 maggio 2026 alle ore 10.00, Marcello PARIS terrà il seminario di crittografia dal titolo "Formal mathematics: improving collaboration and reach. Notes on machinery for Lean 4".
Abstract: Formal mathematics should be handy enough for everyday use, collaborative across labs and individuals, decentralized (allowing possibly different versions of theories and strategies), publishable like papers, and eventually widespread. This talk proposes an add-on to the Lean 4 ecosystem, derived from software-engineering practice as it moves toward mathematics. The machinery is borrowed; the work itself remains mathematics, not software engineering. Concretely: a content-addressed substrate in which every Lean declaration carries a canonical hash derived from its mathematical content, together with a verification system aware of those addresses and operating on top of it. From the substrate, declaration-granular verification, cross-machine sharing, and a federated registry follow. It also makes managing a large formal mathematics project (transcription or native research) tractable: open hypotheses, conditional results, and dependency cascades become first-class registry objects. AI should be both welcomed and under control: producing formal content and consuming it, but kernel-checked, and applied across all of mathematics, not only proof search. As a concrete example, I will mention EM, a sample project I carried out about the Mullin conjecture, built largely by an agent swarm, which conveniently used this setup.
Il seminario si svolgerà in presenza presso il Dipartimento di Matematica e Fisica, Largo San Leonardo Murialdo 1 - Edificio C, Aula C308.
