Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

The "drilling down layer by layer" bit does seem quite well supported:

http://us2.metamath.org:88/mpeuni/konigsberg.html

but you're right about the high-level proofs of the theorems not looking the way most people expect to see proofs.

Perhaps the way that the proofs are broken down (to be accepted by the site) makes it hard to reassemble them at a level of abstraction that is more readable.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: