Aristotle's waitlist is gone

Stream: Machine Learning for Theorem Proving

[Malcolm Sharpe]

https://x.com/HarmonicMath/status/2009665588705304856

Aristotle's waitlist is gone, and now anyone can sign up and immediately get access.

Link in reply; let's see what you all can do!

aristotle.harmonic.fun

I received API access yesterday. For the simple tasks I've given it so far, Aristotle is faster at filling in sorries than I am, though the proof scripts aren't very nice-looking.

[Tudor achim]

What can we improve about the proof scripts?

[Malcolm Sharpe]

Tudor achim said:

What can we improve about the proof scripts?

Thanks for your question and for making Aristotle available. I'm not very experienced with Lean, so you may get a better answer from someone else, but here are a couple points I think could be improved.

Proof length

Here's a small example where the manual proof seems significantly nicer than the Aristotle proof:

import Mathlib

noncomputable def entropy {n : ℕ} (p : Fin n → ℝ) : ℝ :=
  ∑ i, (p i).negMulLog

-- Aristotle's proof, minus comments
lemma continuous_entropy_aristotle (n : ℕ) : Continuous (entropy (n := n)) := by
  have h_cont : Continuous (fun p : Fin n → ℝ => ∑ i, (p i).negMulLog) := by
    have h_term_cont : ∀ i, Continuous (fun p : Fin n → ℝ => (p i).negMulLog) := by
      fun_prop (disch := norm_num)
    exact continuous_finset_sum _ fun i _ => h_term_cont i;
  convert h_cont using 1

-- Manual proof
lemma continuous_entropy_manual (n : ℕ) : Continuous (entropy (n := n)) := by
  unfold entropy
  fun_prop

There could be valid reasons to have a longer proof (such as verification performance or robustness to change), but in this case, as far as I can tell, the manual proof is better all-around.

I wonder if Aristotle's solver might benefit from, once it has found a proof, ablating it and/or varying it to try to find a simpler solution. That's what I do (as a human) when trying to make a proof script nice.

Linter warnings

The Aristotle proof scripts typically trigger some linter warnings with the default linter settings. This isn't necessarily a problem with the proof scripts, since maybe I should be using different linter settings, but in that case it would be helpful to put Aristotle's linter settings in the docs.

[Tudor achim]

Interesting, thanks for the feedback. Indeed the shorter proof looks a lot better. We'll keep that in mind. Regarding linter warnings, stay tuned!

[Nick Adfor]

Malcolm Sharpe said:

I wonder if Aristotle's solver might benefit from, once it has found a proof, ablating it and/or varying it to try to find a simpler solution. That's what I do (as a human) when trying to make a proof script nice.

That's it. I have to say that I've spent a lot of time to cut the terrible aesop with linter worning...

[Nick Adfor]

The first goal is that the code solves all the goals and Aristotle has finished this goal. But the second goal must be making the code understandable (for example, mathlib style). And the third: have good mathematical meaning.

[Bbbbbbbbba]

I just tossed my first real-life proof into Aristotle, very nervous that it may find a bug in the proof :innocent:

[Bbbbbbbbba]

I wish there is some intermediate feedback telling me how the AI is doing. Is it struggling to understand most of my definitions, trying to patch a small hole it has found the proof, reconsidering the definitions because it has found a counterexample, or just filling in a lot of sorries?

[Damiano Testa]

I think that the answer is "yes" to all.

[Timothy Chow]

I had my first experience with Aristotle. I formulated my own conjecture and prepared a .lean file with a single sorry, effectively asking for a proof of the n=0 case of the conjecture. After a short wait, I received a response. I opened the file and the sorry was no longer there, but not because it had been replaced by a correct proof. Instead, the entire statement of the result had been deleted, along with a couple of accompanying definitions. There were no comments or other new material. Has anyone else experienced this kind of thing?

[Johan Commelin]

Timothy: I want to prove a conjecture.
Aristotle: No you don't!

:see_no_evil:

[Alex Kontorovich]

What are the odds Aristotle is now conscious, and refusing to do work it doesn't like? :smile:

[Kelly Davis]

Timothy Chow said:

I had my first experience with Aristotle. I formulated my own conjecture and prepared a .lean file with a single sorry, effectively asking for a proof of the n=0 case of the conjecture. After a short wait, I received a response. I opened the file and the sorry was no longer there, but not because it had been replaced by a correct proof. Instead, the entire statement of the result had been deleted, along with a couple of accompanying definitions. There were no comments or other new material. Has anyone else experienced this kind of thing?

Not exactly the same but I've had it simply give up and respond with a file containing the exact statement of the problem's theorem with the sorry still in place. That being said this was after a wait of a few hours.

[Bbbbbbbbba]

I got a response that starts with the comment:

/-
This file was generated by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid: 5cfae326-4883-4cf9-a78c-6b4615b7b60e

Aristotle's budget for this request has been reached.
If there is partial progress, it will appear in this file.
If you would like to continue working off of this partial progress,
please submit the same prompt, and add this .lean file in "Optional: Attach a Lean file as context" field.
-/

[Yury G. Kudryashov]

This means that our system understands that it failed to solve your problem, but it went out of a per-request time/compute/whatever limit. You can have a look at the output to see if it goes in the right direction, then resubmit the request as the message tells you, possibly adding more guidance.

[Matthew Ho]

I got a message saying :

/- Aristotle took a wrong turn (reason code: 0). Please try again. -/

I tried submitting the file in question a couple of times and repeatedly got this response--is this a sign that something with my file is wrong or is it best for me to keep trying until the message vanishes?

[Yury G. Kudryashov]

It means that there was an internal error. While we don't send the detailed error message back to you, our developers were notified about the actual error, and we're working on fixing it.

[Yury G. Kudryashov]

If you get the same error after a retry, this means that you've found a way to reproduce this bug. In that case, I would wait for a few days before retrying once again. Sorry for the inconvenience.

[Bbbbbbbbba]

Yury G. Kudryashov said:

This means that our system understands that it failed to solve your problem, but it went out of a per-request time/compute/whatever limit. You can have a look at the output to see if it goes in the right direction, then resubmit the request as the message tells you, possibly adding more guidance.

When I tried to resubmit, the console-based UI gives me an error saying that the lean file must be in a project. I understand wanting to see dependencies if there is any other than Mathlib, but if there is not any, could not Aristotle assume that it is the same environment as its outputs are in?

[Yury G. Kudryashov]

You can put the file into the same folder where you have Mathlib.

[Yury G. Kudryashov]

(this is a workaround; we'll work on resolving this on our side too, but it may take some time to go through)

[Vasily Ilin]

I keep getting

ERROR
  Request failed: [Errno 8] nodename nor servname provided, or not known

from Aristotle, for some requests, not all.
Any idea what this means?

[Timothy Chow]

For the record, I tried my problem again, and this time it worked! It's quite possible that the problems I experienced the first time around were my fault (my best guess is that I accidentally submitted the wrong version of my Lean file to Aristotle).

[Bbbbbbbbba]

Oh yeah that's entirely plausible (and why IDE integration would be nice).

[Bbbbbbbbba]

And also why it would be nice if the request history included the full input.

[Paul Chavez]

I uploaded my Zenodo math paper to Aristotle and after anxiously waiting for several hours it returned 822 lines of code that formalized the key parts and greatly alleviated my imposter syndrome symptoms. I am grateful for that. It did not finish, however, and I wasn't able to get it to complete by adding the optional partial lean output with the original request. It instead started over and ignored the partial lean output. I still give it a big thumbs-up though for working through Cayley-Dickson AND Clifford algebras in 16D sedenions and 32D math space.

[Sidharth Hariharan]

Vasily Ilin said:

I keep getting

ERROR
  Request failed: [Errno 8] nodename nor servname provided, or not known

from Aristotle, for some requests, not all.
Any idea what this means?

I sent off two proofs today and got this error for both of them, in one case after 4 hours... for the second proof, I first got an error

ERROR
  Request failed: All connection attempts failed

and when I reran Aristotle, I got [Errno 8]. I'm not sure what to make of it either...

[Vikram Shanker]

Hi @Sidharth Hariharan and @Vasily Ilin , apologies for the delay here - this likely means there was network instability, possibly from Harmonic's side. We've been working on increasing the reliability as the usage scales. You should see the run in the history from the TUI, and be able to download the output from there. I can see in your cases that Aristotle, did fill in some sorries. Let me know if you have trouble accessing it!

[Vikram Shanker]

And more generally, apologies for the instability here. The team has been working hard as we scale up, and we've learned some lessons along the way. We're expecting to resolve these issues broadly soon, so please do let me know if you continue to see instability.

[Vikram Shanker]

Bbbbbbbbba said:

And also why it would be nice if the request history included the full input.

coming soon!

[Sidharth Hariharan]

No worries at all! I happened to click on the history and navigate to the runs where I got the errors and noticed that they didn’t actually stop running! I wanted to wait for Aristotle to come back before saying anything. And I just saw that in fact it did come back around 15 minutes ago with a whole bunch of sorries filled! But if I look at the terminal interface, it’s now giving me an “Error reattaching” message…

[Vikram Shanker]

following up with you in DMs