про мотивацию HoTT
(сохранить на память ссылки, найденные для диалога в другом месте)
Для затравки, линк, недавно размещённый avva -- The Ideal Mathematician -- я это эссе вижу в первый раз, довольно приятно читается. Это одно из эссе из книги "The Mathematical Experience" 1999-го года издания, которую я не читал; два автора -- пожилые американские математики, им уже тогда обоим было за 70 (и оба вроде здравствуют и сейчас). Самоирония, я так понимаю.
Теперь, речь от первого лица с моими выделениями жирным -- мотивация проекта (весьма успешного) нового языка формализации математики (см. HoTT):
The field of motivic cohomology was considered at that time to be highly speculative and lacking firm foundation. The groundbreaking 1986 paper “Algebraic Cycles and Higher K-theory” by Spencer Bloch was soon after publication found by Andrei Suslin to contain a mistake in the proof of Lemma 1.1. The proof could not be fixed, and almost all of the claims of the paper were left unsubstantiated.
A new proof, which replaced one paragraph from the original paper by thirty pages of complex arguments, was not made public until 1993, and it took many more years for it to be accepted as correct. Interestingly, this new proof was based on an older result of Mark Spivakovsky, who, at about the same time, announced a proof of the resolution of singularities conjecture. Spivakovsky’s proof of resolution of singularities was believed to be correct for several years before being found to contain a mistake. The conjecture remains open.
The approach to motivic cohomology that I developed with Andrei Suslin and Eric Friedlander circumvented Bloch’s lemma by relying instead on my paper “Cohomological Theory of Presheaves with Transfers,” which was written when I was a Member at the Institute in 1992-93. In 1999-2000, again at the IAS, I was giving a series of lectures, and Pierre Deligne (Professor in the School of Mathematics) was taking notes and checking every step of my arguments. Only then did I discover that the proof of a key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.
This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.
But this is not the only problem that allows mistakes in mathematical texts to persist. In October 1998, Carlos Simpson submitted to the arXiv preprint server a paper called “Homotopy Types of Strict 3-groupoids.” It claimed to provide an argument that implied that the main result of the “∞-groupoids” paper, which Kapranov and I had published in 1989, cannot be true. However, Kapranov and I had considered a similar critique ourselves and had convinced each other that it did not apply. I was sure that we were right until the fall of 2013 (!!).
Короче, HoTT -- активная борьба с доставшим бардаком, теперь с применением технических средств (в основном Agda, сам Воеводский, по-моему, использует Coq). Новый язык ("univalent foundations") -- более гибкий и выразительный, чем языки старых формализаторских подходов; мне любопытно было бы наблюдать / узнать, получит ли эта деятельность распространение за пределами этой конкретно группы соавторов / единомышленников (объединённых общей специализацией).
Для затравки, линк, недавно размещённый avva -- The Ideal Mathematician -- я это эссе вижу в первый раз, довольно приятно читается. Это одно из эссе из книги "The Mathematical Experience" 1999-го года издания, которую я не читал; два автора -- пожилые американские математики, им уже тогда обоим было за 70 (и оба вроде здравствуют и сейчас). Самоирония, я так понимаю.
Теперь, речь от первого лица с моими выделениями жирным -- мотивация проекта (весьма успешного) нового языка формализации математики (см. HoTT):
The field of motivic cohomology was considered at that time to be highly speculative and lacking firm foundation. The groundbreaking 1986 paper “Algebraic Cycles and Higher K-theory” by Spencer Bloch was soon after publication found by Andrei Suslin to contain a mistake in the proof of Lemma 1.1. The proof could not be fixed, and almost all of the claims of the paper were left unsubstantiated.
A new proof, which replaced one paragraph from the original paper by thirty pages of complex arguments, was not made public until 1993, and it took many more years for it to be accepted as correct. Interestingly, this new proof was based on an older result of Mark Spivakovsky, who, at about the same time, announced a proof of the resolution of singularities conjecture. Spivakovsky’s proof of resolution of singularities was believed to be correct for several years before being found to contain a mistake. The conjecture remains open.
The approach to motivic cohomology that I developed with Andrei Suslin and Eric Friedlander circumvented Bloch’s lemma by relying instead on my paper “Cohomological Theory of Presheaves with Transfers,” which was written when I was a Member at the Institute in 1992-93. In 1999-2000, again at the IAS, I was giving a series of lectures, and Pierre Deligne (Professor in the School of Mathematics) was taking notes and checking every step of my arguments. Only then did I discover that the proof of a key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.
This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.
But this is not the only problem that allows mistakes in mathematical texts to persist. In October 1998, Carlos Simpson submitted to the arXiv preprint server a paper called “Homotopy Types of Strict 3-groupoids.” It claimed to provide an argument that implied that the main result of the “∞-groupoids” paper, which Kapranov and I had published in 1989, cannot be true. However, Kapranov and I had considered a similar critique ourselves and had convinced each other that it did not apply. I was sure that we were right until the fall of 2013 (!!).
Короче, HoTT -- активная борьба с доставшим бардаком, теперь с применением технических средств (в основном Agda, сам Воеводский, по-моему, использует Coq). Новый язык ("univalent foundations") -- более гибкий и выразительный, чем языки старых формализаторских подходов; мне любопытно было бы наблюдать / узнать, получит ли эта деятельность распространение за пределами этой конкретно группы соавторов / единомышленников (объединённых общей специализацией).