Debatten über Computer-Beweise

I have never seen any serious proposals for a vernacular based on set theory. Or to put it another way, as soon as we start expanding and transforming set theory to fit the requirements for $V$, we end up with a theoretical framework that looks a lot like type theory. (You may entertain yourself by thinking how set theory could be used to detect that above does not make sense unless we insert coercions – for if everthying is a set then so are U and V, in which case *does* make sense.)

Möglicherweise als Reaktion auf diese Debatte hat Peter Scholze nun in Buzzards Blog eine Formalisierung seines nach eigener Aussage bisher wichtigsten Theorems vorgeschlagen, einem Satz aus seiner Arbeit mit Dustin Clausen über kondensierte Mathematik:

Let be real numbers, let S be a profinite set, and let V be a p-Banach space. Let be the space of p’-measures on S. Then

for

Im verlinkten Blog erklärt er, worum es geht und warum er diesen Satz wichtig findet. Grob gesagt geht es um eine Algebraisierung der Analysis, wie in jenem Blog erklärt wird. Andere Konzepte aus Scholzes Arbeit wie die perfektoiden Räume waren bereits in Lean formalisiert worden. Mit dieser neuen Herausforderung soll nun wohl endgültig die Rangordnung zwischen den verschiedenen Theorembeweisern geklärt werden:-)

Nachtrag: Zu den grundsätzlicheren Fragen siehe die Diskussion zu Michael Harris‘ Artikel The inevitable questions about automated theorem proving.