[JohnStrange]

It's a pretty cool idea but nothing groundbreaking. There is plenty of AI-driven mathematics already, e.g. the Mizar theorem prover. Pollock used to advocate the idea of continuously trying to prove theorems that might be useful later. It's an underrated idea, in my opinion, and his system of defeasible reasoning based on graph theory is still one of the best.

What's new in this paper is the probabilistic component, trying to guess the outcome of complicated proofs. That's a neat idea, but nothing revolutionary. It may give rise to nice shortcuts for better efficiency.

The real problem is making the machine get a good hunch what to prove, so it doesn't find useful theorems just randomly. I'm not working in this field, so correct me if I'm wrong, but that seems to be rather hard. In any case, as far as I know most automated theorem provers are only semi-automatic, you have to give them an idea about which direction to go and which proof strategy to use.

[chriswarbo]

> The real problem is making the machine get a good hunch what to prove, so it doesn't find useful theorems just randomly. I'm not working in this field, so correct me if I'm wrong, but that seems to be rather hard. In any case, as far as I know most automated theorem provers are only semi-automatic, you have to give them an idea about which direction to go and which proof strategy to use

I'm working in exactly this area, and it's very nice to see it mentioned occasionally as a useful direction!

There's a bunch of nice work being done on this problem; I'm mostly familiar with (roughly chronologically) IsaScheme, IsaCoSy, QuickSpec, Hipspec and Hipster. These take in a bunch of function definitions and output equations about them; they work by enumerating (type-correct) terms and using random testing (QuickCheck) to quickly separate unequal terms from each other, then they apply automated theorem provers to the remainder.

There are also more first-order, less computationally-focused systems for generating theorems out there, like HR and Graffiti.

[tom_mellior]

> AI-driven mathematics already, e.g. the Mizar theorem prover

Can you tell us more about how Mizar is AI-driven? I have never worked with it, but my understanding was that it was a fairly normal proof assistant. That is, proofs are written by humans, and some smallish boring intermediate steps are done using a regular first-order prover. Like with Coq or Isabelle.

Does Mizar do something else as well? Does it use AI to make conjectures?

[JohnStrange]

Not really, I know people who work on Mizar but I'm not myself involved. Anyway it's also subjective what you call AI-driven and what not.

I can comment on another thing, though. Even very simple concepts like well-foundedness conditions go beyond first-order logic and these provers are based on pretty expressive higher-order type systems. AFAIK, they can prove fairly substantial theorems.

[tom_mellior]

I didn't say that the proof assistants were first order! I'm well aware that that's not the case. But AFAIK all the automation they use is first order. Higher order proof steps like "do this by induction on n" are always introduced by hand (at least in Coq and Isabelle), even if the rest of the proof is automatic.

[JohnStrange]

I don't understand what you mean by "all the automation they do is first order". They are based on higher order proof theories, e.g. higher order tablaux, and they implement higher order unification. Otherwise they would be first-order provers and thus much more limited.

But Yes, most common higher-order provers are semi-automatic, you need to give them a hint about which proof strategy to use. That's mainly because they are used that way, not any principal limitation. You won't find many mathematicians who are interested in a theorem prover to spit out some (alleged) theorem by itself, and then let the mathematician check whether it's useful.

The only fully automatic higher-order theorem prover that I know of is ETPS, it will select proof strategies by itself if you don't indicate them. But it's also one of the oldest and slowest and mainly just used for teaching logic.

[tom_mellior]

> I don't understand what you mean by "all the automation they do is first order".

I meant that the tactics of Coq that do reasoning for you, and the internal/external provers of Isabelle, are first order. I was probably partly wrong: you are right that some of them do use higher-order unification. But when in Coq I use "auto" or "omega" or whatever tactic to solve a goal, no higher-order tableaux are in use as far as I know. I have to massage the goal until I get it into a form that is palatable to the first-order automatic provers. Similarly, when I write an Isabelle proof like "from A have B by X; from this have C by Y; hence D by Z", the proof methods X, Y, Z are first order, often off-the-shelf SMT provers. Alternatively, there are also some built-in methods that use simple equational reasoning with higher-order unification, yes.

Let me know if I'm wrong about the details of this! Anyway, none of this means that you cannot prove complex higher-order stuff in these systems. You just can't do it automatically.

And, coming back to the start of this subthread, I don't think Mizar is really different in this regard.