Hacker News new | past | comments | ask | show | jobs | submit login

He got a lot of things right in that video despite being just 2 years involved with mechanised theorem proving. I thought it was a fantastic and inspiring talk.

For example, when he said at the end, that it is obvious to him that this will change how mathematics is done in the future. Yeah, thought the same when I encountered this technology, but I was just a 2nd year math student back then, and Isabelle was developed in the same building. Still, obvious.

When he said that math is more about structure, not so much about induction; yeah, said the same at some ITP more than a decade ago. Got a dismissive question from Andrew Appel when I said that. Tobias Nipkow seemed to agree with the dismissal, I never understood the question though. Didn't get a reply when trying to investigate further on stage :-)

Of course set theory can be automated. I would argue, it can be automated even better than dependent types. Just embed the set theory including Grothendiek universes in simple type theory. The problem here is how to keep the notation sane, as for example + could be defined only once.

Tactic style theorem proving is sooooo old. It is how interactive theorem proving was done from the very beginning. Tactic style proofs are not readable at all except maybe via experiencing them by stepping through them. Declarative proofs are much more readable. Writing declarative proofs with the machine bridging the intermediate steps is the obvious future.

I was always astonished how people can learn stuff. When taking Latin classes, I thought, sure, I can kind of learn to read it, but speak it in real time? No way! But of course, at some point in time people have. Without understanding how.

AlphaGo Zero kind of explains how people can do something really difficult, even strategy based, without exactly knowing what they are doing. This is not much different from how mathematics is done. I think we will have a deep mathematician solving at least one of the remaining millennium problems within the next 20 years. The path starts exactly with how Buzzard and Hales envision it: Bring enough mathematics into one system, so that the millenium problems can actually be stated in the system. Machine learn that stuff. Give feedback to users, they will find it easier to use the system interactively. Create more mathematics. Machine learn that stuff. Rinse repeat.

This can be done. Certainly with 100 million dollars in funding.






It seems like encoding ‘all of math so far’ in some theorem prover seems like an ideal open source project where lots of people can make small contributions which don’t require a vast amount of mathematical knowledge — you’d mostly be simply encoding other people’s results. Is there such an effort now?

I tried to do something like that (http://proofpeer.net), but got lost in the details. Learnt a lot from it, but implementing your own cloud versioning system is probably more appropriate for a project with 100 million dollars funding, not 600000 pounds, half of which goes to university bureaucracy ;-)

I think formal abstracts (https://formalabstracts.github.io) is promising in principle (it doesn't focus on proofs though).

The Archive of formal proofs (https://www.isa-afp.org) is the biggest effort I know, but the logic (Isabelle/HOL) is not powerful enough for doing advanced mathematics comfortably, and the process of contributing is quite arcane.


> It seems like encoding ‘all of math so far’ in some theorem prover seems like an ideal open source project... Is there such an effort now?

Yes. Metamath's set.mm is expressly such a project, and I recently created a Gource visualization of set.mm's progress over time. For the first few years it was basically one person, but that increased over time and there have now been 48 different contributors.

See:

https://www.youtube.com/watch?v=XC1g8FmFcUU


https://formalabstracts.github.io/

Tom Hales' formal abstracts project may be to your liking.


> AlphaGo Zero kind of explains how people can do something really difficult, even strategy based, without exactly knowing what they are doing.

Yet neither does Alpha go. Finding solutions really is an NP-class problem, while proving them is much easier.

> Machine learn that stuff. Give feedback to users, they will find it easier to use the system interactively.

This is interesting. I wonder how much could the computer learn about our natural (or mathematical) language if we were to express problems before coding them, and then feeding both to the ML system.

Going a step further, having the ML system generate the code, and the user correct it (as far as my understanding of deep learning goes, correcting a net's output and backfeeding it is currently strictly equivalent to just providing that data in the training set before performing stochastic gradient descent. We might be missing something here, as it is obviously much more effective with us, and that would make ML a lot eaier to work with, requiring less training data).


> Yet neither does Alpha go. Finding solutions really is an NP-class problem, while proving them is much easier.

That's not really true. Proving that an already found solution is correct might be easy for certain solutions (that's the whole idea of proof certificates). But finding a proof for an arbitrary theorem is certainly not easy. And that is what mathematicians do. Here, finding the proof IS finding the solution.


Of course, but when you have found a proof, verifying that it is correct is fairly trivial (if tedious by human standards, it's only verifying that each statement is correct).

I meant proving in the sense of "checking that the solution works". In a mathematical problem, the solution would be a tentative proof for a theorem. Proof which needs to be verified. I should probably have used "verify" instead of "prove" in this context.


It is not difficult to keep the notation sane in formalizations based on set theory. One way is to defer overloading of symbols to the presentation layer. You can see an example of that at [1] where the + sign is used to denote the group operation, right and left shifts on sets and the natural "addition" of subsets of the group derived from the group operation.

[1] http://isarmathlib.org/TopologicalGroup_ZF.html


> It is not difficult to keep the notation sane in formalizations based on set theory.

Keeping notation sane is, of course, very important. I think keeping notation sane is harder than it might first appear, but it is certainly possible.

One interesting trick used by Metamath's set.mm is to define variables that look similar to operators but can be defined for purposes of a particular proof (e.g., as hypotheses). For example, + underline, * underline, and so on.

For an example, see theorem grpridd, "Deduce right identity from left inverse and left identity in an associative structure (such as a group)." http://us.metamath.org/mpeuni/grpridd.html - the hypotheses include statements about "+ underscore", and lead to a proof about + underscore.


If it can be done, it needs to be done at the presentation layer, I guess so too.

It has been a while since I worked with Isabelle locales. So how come that in your example "x + y" is not being confused with "A + B", although all involved entities are ZF sets? Or does A actually have a different type than x ?


Isabelle allows the user to define symbols. So, those two operations are represented by different symbols in the source (the *.thy files) but the presentation layer renders them both as "+". You may want to look at the corresponding IsarMathLib source at [1] on GitHub. Isabelle/ZF uses only two types: set ("i") and prop("o").

[1] https://github.com/SKolodynski/IsarMathLib/blob/master/IsarM...


Ah, I see. So, when I type in those formulas, can I use + or do I need to type in the original symbols?

Nevermind, I know the answer to that. That's why Set theory notation is a difficult problem, and you need some sort of type presentation / input layer. Some people also refer to that as a user space type system or soft types: https://www21.in.tum.de/~krauss/publication/2010-soft-types-...


> Writing declarative proofs with the machine bridging the intermediate steps is the obvious future.

Do you have a take on what systems are best for this? I found Isabelle/HOL quite reasonable in this respect. There are some toy add-ons to Coq, but I don't think any of them work. There's also FStar which has Z3 integration (if I recall correctly), but last time I played with it it needed quite a lot of hand-holding.


Yes, Isabelle is the best system for this style of proving right now.

Would you mind suggesting an introductory text for this stuff?


Great recommendation, thanks!

Kind of embarrassing, but I cannot! The thing is, development of mechanised theorem proving has been driven by computer scientists, so proving program correctness, doing programming language semantics, and explaining constructive ideology is at the heart of most introductory text books.

I would recommend just following the "Theorem Proving in Lean" book for starters.


Tutorial on CoQ, a proof assistant

https://news.ycombinator.com/item?id=21185624




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

Search: