[submission] mem_convexHull_finset_extremePoints_of_mem_compact_convex via Aristotle (Harmonic)

[kim-em]

Submission URL

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

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.