Ruka hadi maudhui
The Lumenary
Njia za utafitiComputationSomo linapatikana

Formalising published mathematics

Optional research direction: turning published mathematics into machine-checked proofs, using blueprints that link informal statements to formal ones, collaborating on large projects, and contributing to libraries such as Mathlib.

math.comp.formalising-published-mathematics

Fungua somo Onyesha kila kinachohitajika kufikia mada hii

Inajengwa juu ya

Formalising mathematics in Lean and MathlibType theory and propositions as typesReading the mathematical literature

Masharti ya awali ya lazima 22 (hadi chini kabisa)

Utajifunza

  • Write a blueprint that breaks a published theorem into formalisable lemmas and records their dependencies.
  • Formalise a short published result, recording any gaps or implicit assumptions found along the way.
  • Describe completed large formalisations and what they did and did not verify.

Fasili

  • A blueprint is a document linking each informal definition and lemma to its formal counterpart and recording the dependencies between them.
  • The trusted base of a formal proof is what must be trusted for the check to be meaningful: the proof checker's kernel, the axioms used and the formal statement.

Nadharia

  • The Liquid Tensor Experiment formalised a central theorem of Clausen and Scholze's condensed mathematics in Lean; it was completed in 2022.
  • The Feit–Thompson odd order theorem was formalised in Coq by Gonthier and collaborators (2012).
  • Formalisation verifies the proof of the formal statement; whether that statement faithfully captures the published theorem must be checked by people.

Mawazo potofu ya kawaida

  • Thinking formalisation makes peer review unnecessary.
  • Believing a formal proof follows the informal paper line by line; formal proofs often reorganise the argument substantially.

Ugunduzi wa hiari

Njia za kujifunza

Usomaji zaidi