0:00-36:32
Streams straight from the publisher. podnod never proxies or re-hosts episode audio.
“Es gibt Beweise mit Löchern, Beweise mit Fehlern und Beweise, die nur zwei Leute auf der ganzen Welt verstehen. […] Um wirklich zu wissen, welche Resultate man glauben kann, muss man Teil eines inneren Zirkels sein und Zugang zu den Experten haben, die den Konsens herstellen.” sagt Kevin Buzzard.
Oder man beweist die Sätze formal.
- Formale Theorembeweiser
- Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started | SpringerLink
- Isabelle
- The Foundation of a Generic Theorem Prover
- Lean
- Xena | Mathematicians learning Lean by doing.
- The Natural Number Game - Lean spielend lernen.
- Building the Mathematical Library of the Future | Quanta Magazine
- The liquid tensor experiment
- Proof Assistant Makes Jump to Big-League Math
- Liquid tensor experiment | Xena
- Half a year of the Liquid Tensor Experiment: Amazing developments | Xena
- Philosophisches
- Pure maths in crisis? | plus.maths.org
- Will Computers Redefine the Roots of Math? | Quanta Magazine
- The philosophy of mathematics
Feedback gerne an feedback (bei) pi-ist-genau-3.de
Isabelle
isabelle.in.tum.deThe Foundation of a Generic Theorem Prover
cl.cam.ac.ukLean
leanprover.github.ioXena | Mathematicians learning Lean by doing.
xenaproject.wordpress.comThe Natural Number Game - Lean spielend lernen.
ma.imperial.ac.ukBuilding the Mathematical Library of the Future | Quanta Magazine
quantamagazine.orgProof Assistant Makes Jump to Big-League Math
quantamagazine.orgLiquid tensor experiment | Xena
xenaproject.wordpress.comHalf a year of the Liquid Tensor Experiment: Amazing developments | Xena
xenaproject.wordpress.comPure maths in crisis? | plus.maths.org
plus.maths.orgWill Computers Redefine the Roots of Math? | Quanta Magazine
quantamagazine.orgThe philosophy of mathematics
dpmms.cam.ac.uk
