Aristotle and axioms

Stream: Machine Learning for Theorem Proving

[Mark Ettinger]

I've started to experiment with Aristotle and I had a file rejected with errors as it contained axioms (regarding the assumptions of special relativity). Are axioms fundamentally incompatible with Aristotle and, if so, do I have any alternative other than proving A --> B instead of B (for every statement B) where A is a conjunction of all my axioms?

[Yan Yablonovskiy 🇺🇦]

Mark Ettinger said:

I've started to experiment with Aristotle and I had a file rejected with errors as it contained axioms (regarding the assumptions of special relativity). Are axioms fundamentally incompatible with Aristotle and, if so, do I have any alternative other than proving A --> B instead of B (for every statement B) where A is a conjunction of all my axioms?

Afaik a work around is stating your assumptions as lemmas with by admit rather than sorry (or rather than using axiom, just if you used sorry Aristotle would try fill it rather than take it as an assumption ).

[Wen Yang (杨文)]

Yan Yablonovskiy 🇺🇦 said:

Afaik a work around is stating your assumptions as lemmas with by admit rather than sorry .

I tried the by admit workaround yesterday, but unfortunately Aristotle still behaved as if they were sorrys, despite my prompt explicitly asking it to "replace the sorrys".

[Yury G. Kudryashov]

What was your command line? Or which option did you use in the TUI? Or was it Web UI?

[Mark Ettinger]

I used the command line program to submit with the option to replace all sorries. But I converted everything as I described in the original message, i.e. axioms to implications and it all worked out fine. Aristotle is remarkable! At first I used all my lemmas which I had developed when doing everything by hand. Then, just for fun, I asked Aristotle to prove the main theorem directly which previously had taken me several pages of code, and it (he/she/they?) delivered a dense proof in about 10 lines. I then stated two more theorems and Aristotle proved them also in short order. Takeaway lesson: first try to let Aristotle do _everything_ before doing any work. I guess the downside is that the formal proof carries none of the geometric intuition of the original. Which raises all sorts of interesting philosophical questions.....

[Yury G. Kudryashov]

Note: if you're getting a short proof from Aristotle, there are chances that

• either the "main" part of your goal is already in Mathlib;
• or that you forgot some assumption line n > 0 somewhere, and Aristotle exploited this.

[Mark Ettinger]

I was indeed worried that it was too good to be true. I'm far from a Lean expert so if you have any desire to view the file: https://github.com/mettinger/Relativity/blob/main/relativity.lean

[Yury G. Kudryashov]

Which theorem?

[Mark Ettinger]

If there is something fishy going on I would guess it would show up in any of the three but the first one is slowerThanLight.

[Aaron Liu]

Mark Ettinger said:

I was indeed worried that it was too good to be true. I'm far from a Lean expert so if you have any desire to view the file: https://github.com/mettinger/Relativity/blob/main/relativity.lean

Aristotle seems to be doing the same thing for all three proofs, which is to exploit a typo in axsm to show there cannot be any inertial observers, and so any theorem that assumes inertial observers as a hypothesis is vacuously true.

[Mark Ettinger]

Interesting. Thanks! Back to work.

[Wen Yang (杨文)]

I encountered an issue but wasn't sure where to report it to the developers. If any developers see this post, perhaps you could look into the specific process:

This project request had uuid: 964adaad-7b5c-49af-8b27-20f6bab24d9f

When I provided the following in the prompt:

theorem name1 hypothesis1 : conclusion1 := by admit

and requested to "replace the sorrys (but not admits)", Aristotle generated an output.lean file that transformed it into:

variable (name1 : hypothesis1, conclusion1)

As a result, Aristotle failed to complete the proof. I suspect the reason is that after this transformation, the theorem name1 can no longer be referenced to prove other statements.

[Alex Meiburg]

Yes, it looks like that prevented the theorem from being loaded properly, since the resulting declaration gives an error. That's an unusual failure case! Thanks for the report!