Converting most of existing math into formal developments suitable for computer use would be a huge undertaking, possibly requiring several hundred man-years of work. Most people aren't going to work on such a goal with any seriousness until it's clear to them that the results will in fact be widely used. This in turn requires further work in order to come up with lightweight, broadly-applicable logical foundations/frameworks, as well as more work on the usability of proof environments. Progress on these things has been quite slow, although we have seen some encouraging news lately, such as the recent 'formal proof' of the Kepler conjecture. And even that was actually a bunch of formal proofs developed under quite different systems, that can be argued to solve the conjecture only when they're somehow combined. I think this example makes it abundantly clear that current approaches to this field - even at their most successful - do have non-trivial drawbacks.

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.

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.