Computer theorem proving and HoTT

Se ha publicado un artículo sobre la demostración asistida por ordenador y los fundamentos de la matemática titulado Computer theorem proving and HoTT.

Sus autores son Joe Leslie-Hurd (de Intel Corporation) y G. McC. Haworth (de la Universidad de Reading).

Su resumen es

Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the ‘LT’ Logic Theory Machine of Newell, Shaw and Simon. In game-playing terms, the ‘initial position’ is the core set of axioms chosen for the particular logic and the ‘moves’ are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting ‘HoTT’ book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.