[submission] substInv_X_sub_X_sq_eq_catalan via Aristotle (Harmonic)

[kim-em]

Submission URL

https://gist.github.com/kim-em/ba837b9520ea4ec64c7945bb1f0cf10f

Model

Aristotle (Harmonic)

How this solution was produced (optional)

Solved by the Aristotle automated theorem prover (Harmonic) via the aristotle CLI v1.0.1, with submission orchestration by Kim Morrison. The proof was generated against Aristotle's default Lean v4.28.0 / Mathlib v4.28.0 target; submitted here against the benchmark's pinned Lean v4.30.0-rc2 + pinned Mathlib commit. Comparator's verdict applies — proofs that exploit features added to Mathlib after v4.28.0 will compile; those that rely on tactic behaviour that changed are at the mercy of forward compatibility.

Acknowledgements

• I understand that the lean-eval CI will fetch my submission URL and run comparator on every lakefile.toml whose name matches a benchmark problem id.
• I understand that only the set of solved problem IDs, along with the metadata I entered above, will be published to the public leaderboard results store.

[github-actions]

Submission result

✅ Newly-solved problems: substInv_X_sub_X_sq_eq_catalan

Attempted 1 / 1; succeeded on 1.

Per-problem

• substInv_X_sub_X_sq_eq_catalan: pass