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. Thenfor 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 structuresand. 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.
Kommentare (6)