|
|
Graphs on surfaces and curves over number fields
April 15, 2020 18:30–20:00, Moscow, online
|
|
|
|
|
|
Верификация длинных доказательств: мечты, планы и реальность
G. B. Shabatab a Institute for Theoretical and Experimental Physics named by A.I. Alikhanov of National Research Centre «Kurchatov Institute»
b Russian State University for the Humanities, Moscow
|
Number of views: |
This page: | 203 |
|
Abstract:
We will mainly talk about the unfinished project of Vladimir Voevodsky (the preliminary result of which is summarized in the collective monograph [1]), in which it was supposed to significantly expand the interaction of mathematicians with computers in the construction and verification of proofs.
After a brief overview of the univalent foundations of mathematics, attention will be focused on the problems that arise in connection with proofs, the traditional understanding of which is difficult or impossible due to their length and complexity. Examples will be given; the position of the speaker will be critically compared with the provisions of the well-known provocative text of Nikolai Vavilov [2].
In conclusion, considerations will be expressed about the formalization of the taught mathematics.
[1] Homotopy Type Theory: Univalent Foundations for Mathematics. Univalent Foundations Project, Institute for Advanced Study, 2013. (465 pages) arXiv: 1308.0729
[2] Nikolai Vavilov. Reshaping the metaphor of proof. Philosophical Transactions of the Royal Society A. Mathematical, Physical, and Engineering Sciences, 2019. DOI: 10.1098 / rsta.2018.0279
The meeting will be combined with the Research Seminar on Mathematical Logic of the Department of Mathematical Logic and Theory of Algorithms, link to the recording of the seminar: http://lpcs.math.msu.su/rus/nis.htm.
|
|