Kategorier
Blog Matematik

Et fornyet løfte

Zorns Lemma i Lean (http://www.andrew.cmu.edu/user/avigad/itp/)

I januar 2019 var jeg til POPL2019 i Cascais i Portugal, og her købte jeg bl.a. Adam Chlipalas bog Certified Programming with Dependent Types om bevisassistenten Coq. Jeg lovede højt og helligt alle, jeg mødte til POPL2019, at jeg ville lære Coq og give mig til at formalisere alle mine matematiske anstrengelser. Men i 2019 fik jeg travlt, meget mere travlt end jeg ville have anet eller ønsket mig – og det væltede frem med bekymringer. I efteråret blev jeg f.eks. syg og fik en overgang alt for meget at tænke på, som jeg ville ønske, jeg aldrig skulle have tænkt på. Jeg endte ikke desto mindre med at vejlede et spændende speciale om bevisassistenten Agda, så nogle andre fik lært at bruge en bevisassistent til noget fornuftigt – og selv fik jeg også brugt Agda en smule, uden at jeg dog følte, at jeg kom dybt ned i materien.

I år har jeg nævnt bevisassistenter og formaliseret matematik for matematikere, jeg kender. De synes at det lyder rigtig spændende (for det er det jo). Så snart skal det være, og hermed afgiver jeg et fornyet løfte: I 2021 skal det være. Jeg er især opmuntret af at læse om hvordan nogle “rigtige” matematikere som Kevin Buzzard fra Imperial College har taget bevisassistenten Lean til sig. Lean er baseret på Calculus of Constructions ligesom Coq.

Når Buzzard udtaler at

I am a pure mathematician, a professor at Imperial College London. Two years ago I started experimenting with the Lean Theorem Prover (written by Leo de Moura at MSR). I now clearly understand that software such as Lean is part of the inevitable future of mathematics. And right now, I can say with high confidence that Lean is easily the most promising of the theorem provers currently available.
Clear: tools such as Lean will one day help us mathematicians search for theorems in the literature, and help us to prove theorems. These tools may also change the way we teach.

Fra Kevin Buzzard: The future of mathematics?, 5th September 2019 (https://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf)

er der noget at tænke over, og ikke kun for mig. Det er især spændende at vide, at der nu er en systematisk indsats for at bygge et bibliotek med ordentlige, formaliserede beviser for matematik, formaliseret i Lean. Det er der en god artikel om i Wired.