Aristotle Lean
Trit: -1 (MINUS) Domain: Formal Verification / Theorem Proving Provider: Harmonic (harmonic.fun)
Overview
Aristotle is an IMO Gold Medal level Lean4 theorem prover that fills sorry holes in proofs, auto-generates counterexamples for false statements, and integrates with Mathlib and lake dependencies.
API Configuration
Endpoint: aristotle.harmonic.fun
Auth: Auth0-based (requires signup/login at harmonic.fun)Capabilities
- Sorry Hole Filling: Completes incomplete Lean4 proofs
- Dual Input: Accepts English descriptions or Lean4 code
- Counterexample Generation: Auto-generates counterexamples for false statements
- Project Integration: Works with project theorems, lake dependencies, Mathlib
- PROVIDED SOLUTION Tag: Use comment tag to mark solution regions
Benchmarks
| Benchmark | Score |
|---|---|
| MiniF2F | 90% |
| VERINA | 96.8% |
Usage Pattern
-- English prompt in comment
-- "Prove that the sum of two even numbers is even"
theorem sum_even (a b : ℕ) (ha : Even a) (hb : Even b) : Even (a + b) := by
sorry -- Aristotle fills this-- PROVIDED SOLUTION: explicit solution marker
theorem my_theorem : P → Q := by
-- PROVIDED SOLUTION
sorryIntegration with GF(3)
This skill participates in triadic composition:
- Trit -1 (MINUS): Verification/validation/analysis
- Conservation: Σ trits ≡ 0 (mod 3) across skill triplets
Related Skills
- lean4-metaprogramming (trit +1)
- mathlib-tactics (trit 0)
- proof-assistant (trit -1)
- formal-verification (trit -1)
Skill Name: aristotle-lean Type: Formal Verification / Theorem Proving Trit: -1 (MINUS) GF(3): Conserved in triplet composition
Non-Backtracking Geodesic Qualification
Condition: μ(n) ≠ 0 (Möbius squarefree)
This skill is qualified for non-backtracking geodesic traversal:
- Prime Path: No state revisited in skill invocation chain
- Möbius Filter: Composite paths (backtracking) cancel via μ-inversion
- GF(3) Conservation: Trit sum ≡ 0 (mod 3) across skill triplets
- Spectral Gap: Ramanujan bound λ₂ ≤ 2√(k-1) for k-regular expansion
Geodesic Invariant:
∀ path P: backtrack(P) = ∅ ⟹ μ(|P|) ≠ 0
Möbius Inversion:
f(n) = Σ_{d|n} g(d) ⟹ g(n) = Σ_{d|n} μ(n/d) f(d)SDF Interleaving
This skill connects to Software Design for Flexibility (Hanson & Sussman, 2021):
Primary Chapter: 4. Pattern Matching
Concepts: unification, match, segment variables, pattern
GF(3) Balanced Triad
aristotle-lean (−) + SDF.Ch4 (+) + [balancer] (○) = 0Skill Trit: -1 (MINUS - verification)
Connection Pattern
Pattern matching extracts structure. This skill recognizes and transforms patterns.