Debatten über Computer-Beweise

In computerüberprüfbaren Beweisen sehen manche die Zukunft der Mathematik. Darüber, auf welchen formalen Grundlagen man Computerbeweise aufbauen sollte, gab es in den letzten Wochen einige hitzige Debatten.

An möglichen Grundlagen für die Mathematik und insbesondere für formale Theorembeweiser gibt es neben der von den meisten Mathematikern verwendeten Mengenlehre („set theory“) noch verschiedene Arten von Typentheorien: „simple type theory“, „dependent type theory“ und „homotopy type theory“. Letztere, auch als univalente Grundlagen bezeichnet, wurde vor allem von Wladimir Wojewodski propagiert, der leider vor drei Jahren verstorben ist.

Die jüngste Debatte war durch einen schon vor über einem Jahr von Kevin Buzzard gehaltenen Vortrag „The Future of Mathematics“ ausgelöst worden.

In diesem Vortrag hatte er vertreten, dass der auf „dependent type theory“ beruhende Beweisassistent Lean als einziger in der Lage sei, alle Mathematik zu formalisieren.

Große Aufmerksamkeit bekam dieser Vortrag durch eine am 19. November auf mathoverflow gestellte, bisher 17000 mal gelesene Frage What makes dependent type theory more suitable than set theory for proof assistants?. In der Diskussion dazu wird recht deutlich, dass auf Typentheorie basierende Beweiser bisher mehr leisten als auf Mengenlehre beruhende, und dass mit den univalenten Grundlagen bisher wenig umgesetzt wurde (während in Coq, was auf ähnlichen Grundlagen beruht, aber auch ein paar mit univalenten Grundlagen nicht mögliche Dinge kann, schon viel an Algebra implementiert wurde bis hin zum Satz von Feit-Thompson mit seinem ursprünglich 254 Seiten langen Beweis).

Die mit Abstand meisten Upvotes erhielt die Antwort von Andrej Bauer. Ein Auszug daraus:

Mathematicians omit a great deal of information in their writings, and are quite willing to sacrifice formal correctness for succinctness. The reader is expected to fill in the missing details, and to rectify the imprecisions. The proof assistant is expected to do the same. To illustrate this point, consider the following snippet of mathematical text:

– Let U and V be vector spaces and a linear map. Then for all x and y.

Did you understand it? Of course. But you might be quite surprised to learn how much guesswork and correction your brain carried out:

* The field of scalars is not specified, but this does not prevent you from understanding the text. You simply assumed that there is some underlying field of scalars K. You might find out more about K. in subsequent text. (K. is an existential variable(https://coq.inria.fr/refman/language/extensions/evars.html).)

* Strictly speaking ““ does not make sense because U and V are not sets, but structures and . Of course, you correctly surmised that f is a map between the *carriers*, i.e., . (You inserted an implicit coercion(https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html) from a vector space to its carrier.)

* What do x and y range over? For f(x) and f(y) to make sense, it must be the case that and . (You inferred(https://en.wikipedia.org/wiki/Type_inference) the domain of x and y.)

* In the equation, + on the left-hand side means , and + on the right-hand side , and similarly for scalar multiplication. (You reconstructed the implicit arguments(https://coq.inria.fr/refman/language/extensions/implicit-arguments.html) of +.)

* The symbol 2 normally denotes a natural number, as every child knows, but clearly it is meant to denote the scalar . (You interpreed “2“ in the notation scope(https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes) appropriate for the situation at hand.)

The vernacular V must support these techniques, and many more, so that they can be implemented in the elaborator. It cannot be anything as simple as ZFC with first-order logic and definitional extensions, or bare Martin-Löf type theory. You may consider the development of $V$ to be outside of scope of mathematics and logic, but then do not complain when computer scientist fashion it after their technology.

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.