874: Structural Proof Theory/6

[Buzzard, Kevin M]

HF:

You can view a proof as a series of what I call HAVE/WANT
statements... So this is ENTIRELY HIGHLY USER DRIVEN, with the
computer making its best judgments on its list of suggestions, so
hopefully NORMALLY the user can spot their favorite moves just looking
at the top of the list of possible moves. WHAT IS THE STATE OF THE ART
HERE?

Me: Yeah, that. The computer looks at the top of the list of possible moves.
There is scope for more here, but the "ideas" which you need for more clever
solutions to "exists a : X such that..." are probably domain dependent?

HF:

4. THE USE OF PROOF TECHNOLOGY TO CREATE NEW KINDS OF ELECTRONIC TEXTBOOKS.

Me: this is one of my motivations right now. The problem is that first we have
to make sure we have a system in which users can do mathematics in the fluid
way in which they do it on paper. This is work in progress.

HF:

5. There are some reports of proof technology FINDING ERRORS by
refusing to accept things they were expected to accept. And then
helping find the fix.

Me: I think this is an oversimplificcation. I am not sure the ATP
(automatic theorem proving) machines do this, and with the ITP systems
what happens is no different to the situation where the graduate student
is explaining their proof of 0 = 1 to the advisor -- the advisor grills them
on the details and eventually the proof unravels. It is the user who finds
the problem in some sense -- if the user doesn't understand all the
details of the mathematics then they can't expect the computer to.
Expecting a computer to fix up a bad human proof is asking rather a lot
right now. Some of the answers here are interesting:

https://mathoverflow.net/questions/291158/proofs-shown-to-be-wrong-after-formalization-with-proof-assistant

HF

6. There are reports of proof technology GENERATING CONJECTURES. I
don't know much about this, but I know that at least this is very
powerful in Euclidean Geometry from decades back.

Me: My limited experience with this was looking at output of a computer
program which was generating conjectures about sequences of naturals
by looking for relations between sequences in the OEIS (https://oeis.org/).
I didn't see anything which wasn't either (a) trivially true, (b) trivially false
or (c) followed from a known conjecture, which was disappointing.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210321/50986157/attachment-0001.html>