Formalizing Mathematics

[gusl]

The QED Manifesto: What Is the QED Project and Why Is It Important?

Also, try reading some theorems from http://mizar.uwb.edu.pl/JFM/ . Volume is really basic stuff while Volume 15 has theorems about algebraic geometry. I really don't see why mathematicians can't work more like this. A little interface work could go a long way.

Comments

[easwaran.livejournal.com]

Hmm... reasons 4 and 5 seem unconvincing to me, and perhaps even premised on falsehood. I don't see how formalizing all of mathematics would impress people more with its beauty, and somehow convince them of "the reality of truth" - rather, I think it would convince them of the arbitrariness of truth.