You're speaking of unifying all of math under the same system. I don't think that's strictly necessary, or even desirable. The computer science equivalent of that would be a development environment where every algorithm in the literature is implemented as a function.

I'm wondering more about why problem-specific computer-verifiable proofs aren't used.

The problem is, no matter how 'problem-specific' your proofs are, they aren't going to be 'verifiable' unless you specify them all the way down to some reasonable foundation. That's the really big undertaking, so you'll want to unify things as much as possible, if only to share whatever you can and avoid any duplication of effort.

Open thread, Nov. 23 - Nov. 29, 2015

by MrMind 1 min read23rd Nov 2015258 comments


If it's worth saying, but not worth its own post (even in Discussion), then it goes here.

Notes for future OT posters:

1. Please add the 'open_thread' tag.

2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)

3. Open Threads should be posted in Discussion, and not Main.

4. Open Threads should start on Monday, and end on Sunday.