Vladimir Voevodsky, a mathematical prodigy who dedicated his life to an error-detection program died at age 51.
We tend to boast that mathematical truths are eternal. Unlike other disciplines, where theories considered correct can be refuted in the light of new results, mathematicians, when we demonstrate a theorem, know that it will be valid forever. But in practice, when we finish writing the demonstration, there is always doubt: will there be any error in reasoning? Our system of publication and dissemination of results establishes several filters that must pass the text before it is considered correct and incorporated into the scientific literature: we review the work in detail; we explain it to colleagues, trying to convince them of its validity; we expose our results on the internet where all mathematicians can see them; and we send the article to a scientific journal in which the editor, before publishing, sends it to an expert in the area, whose job is to check that there are no errors, as well as evaluate if the result is interesting enough for publication. However, although it may be disturbing, these processes are not infallible, and sometimes fail to yield incorrect results.
In 1998, the mathematician Carlos Simpson ran into one of them. A theorem that had been enunciated in 1989 by Vladimir Voevodsky could not be true, for he had found a very complicated example where he was not satisfied. Voevodsky's demonstration was so technical that Simpson was also unable to find the verdict that the reviewers had overlooked at the time. Voevodsky's demonstration, or Simpson's counterexample, was not known for a long time, until Voevodsky located the judgment in his reasoning in 2013. In 2000 they found another error in another of his works, which since its publication in 1993 had been studied and validated by experts.
This produced a deep impression on Voevodsky, considered one of the great mathematicians of his generation, an expert in abstract algebraic geometry and recipient of a Fields medal in 2002. He then decided to abandon his usual research for the moment and to look for a way to check automatically mathematical reasoning to detect the errors hidden in the demonstrations, which threatened to pierce the solid building of mathematics.
In principle any demonstration can be written, starting from some hypotheses and following well defined logical rules, so that a machine could check the validity of each step. In practice this is not possible, since the hypotheses on which mathematics are based are set theory, and it is so far removed from the kind of arguments used in current research that formalizing a demonstration to the last detail would be a work impotent impossible to realize. But what if there were another theory on which mathematics could be based and with which it would be feasible to write demonstrations that a machine could verify?.
There has already been progress in this direction, replacing set theory by type theory, following ideas that come from theoretical computing. In 2012, the team led by Georges Gonthier culminated a demonstration that a computer can check from Feit-Thompson's theorem, an important result of group theory of 1963. Voevodsky incorporated ideas of topology and algebraic geometry in type theory.
If we were able to advance to a sufficiently simple system, such as for mathematicians to use in our usual work, it will be a real revolution. In addition to avoiding the problem of hidden errors, it would release the arduous work of verification and revision to the mathematical collective. And it would solve situations like the mathematician Shinichi Mochizuki and his supposed demonstration of the so-called ABC conjecture, which the scientific community, despite their efforts, is not able to validate. On the other hand, these ideas could also be used to verify that software programs do not contain errors that lead to system failures.
Born in Moscow in 1966, Voevodsky was a young prodigy who immediately attracted the attention of his teachers. After the fall of the Berlin wall, he obtained his doctorate in Harvard and obtained a permanent place in the prestigious Institute for Advanced Studies, in Princeton. His research focused on the use of topology ideas to study problems of algebraic geometry. In that field he resolved certain conjectures in algebra, the so-called Milnor and Bloch-Kato conjectures, of great interest to the community. In 2002 he won the Fields medal, one of the most prestigious prizes in mathematics. He managed to take significant steps in his error detection program but, much less, to reach the complete refundamentación he was looking for. On September 30, just 51, he died in Princeton. We hope that his vision and his commitment prevail and, in the wake of his ideas, the revolution he pursued can be reached.
