Aristotle Partial Results

Stream: Machine Learning for Theorem Proving

[Kelly Davis]

For amusement I often submit "hard" problems to Aristotle, e.g. erdos_N.lean.

Usually the result is, it works on the problem for a bit, then simply "gives up", e.g. returning erdos_N_aristotle.lean which is the sorry proven statement I submitted but with a comment indicating the file was generated by Aristotle.

While this behavior is understandable, Harmonic has finite compute, what would be of more use would be for it to return partial results, e.g. what it tried and what failed.

This would be useful information in trying to understand how to approach the problem and how not to approach the problem. This type of information is available when running against other LLM's when one sees the thinking they are engaged in; so, I assume it's available.

I wonder if others would find this of use and maybe Harmonic could take this as a feature request?

[Vasily Ilin]

I agree.
Another feature request of mine is to include the prompt in the generated comment. Because I often try several prompts for the same problem to see which works better, but then I forget which one was which.