Category Archives: proof assistants

Two kinds of mathematics

Preliminary reading: “The Origins and Motivations of Univalent Foundations” by V.¬†Voevodsky’s [PDF] “Proofs and refutations” by I. Lakatos [link] “On proofs and progress in mathematics” by W. Thurston [link] I find the recent surge in interest in the use of … Continue reading

Posted in armchair philosophy, proof assistants | 1 Comment

Searching/fumbling for a proof assistant

I was always very impressed with people who use proof assistants to do their maths. It seems like something from the future, mechanised, unerring, complicated, slightly incomprehensible, and it makes traditional pen-and-paper (well, LaTeX) maths seem quaint, artisanal, even obsolete. … Continue reading

Posted in proof assistants | 4 Comments