Professor Voevodsky’s Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes
In January 1984, Alexander Grothendieck submitted to the French National Centre for Scientific Research his proposal “Esquisse d’un Programme.” Soon copies of this text started circulating among mathematicians. A few months later, as a first-year undergraduate at Moscow University, I was given a copy of it by George Shabat, my first scientific adviser. After learning some French with the sole purpose of being able to read this text, I started to work on some of the ideas outlined there.
In 1988 or 1989, I met Michael Kapranov who was equally fascinated by the perspectives of developing mathematics of new “higher-dimensional” objects inspired by the theory of categories and 2-categories.
The first paper that we published together was called “∞-Groupoids as a Model for a Homotopy Category.” In it, we claimed to provide a rigorous mathematical formulation and a proof of Grothendieck’s idea connecting two classes of mathematical objects: ∞-groupoids and homotopy types.
Later we decided that we could apply similar ideas to another top mathematical problem of that time: to construct motivic cohomology, conjectured to exist in a 1987 paper by Alexander Beilinson, Robert MacPherson (now Professor in the School of Mathematics), and Vadim Schechtman.
In the summer of 1990, Kapranov arranged for me to be accepted to graduate school at Harvard without applying. After a few months, while he was at Cornell and I was at Harvard, our mathematical paths diverged. I concentrated my efforts on motivic cohomology and later on motivic homotopy theory. My notes dated March 29, 1991, start with the question “What is a homotopy theory for algebraic varieties or schemes?”
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.READ MORE>