Podcasts Technology Iowa Type Theory Commute Technical reasons for lack of adoption of computer-checked proofs

Technical reasons for lack of adoption of computer-checked proofs

Published: Nov. 28, 2019, 6 p.m.

b'

Discussion of a technical reason for lack of adoption of computer-checked proofs for mathematics, namely the level of detail in the proof.\\xa0 Proof assistants require too much detail in proofs to allow mathematicians to carry over their elegant art of expressing just the right amount of information to convey the idea of the proof to a mathematically competent reader.\\xa0 For Computer Science, a problem of adoption is that proofs are computationally useless (generally).

'