Stats
Actions
Tags
From asi
Fills Lean4 sorry holes in proofs, generates counterexamples for false statements, and handles English/Lean4 inputs via Harmonic API. For formal verification with Mathlib/lake.
How this skill is triggered — by the user, by Claude, or both
Slash command
/asi:aristotle-leanThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
**Trit**: -1 (MINUS)
Trit: -1 (MINUS) Domain: Formal Verification / Theorem Proving Provider: Harmonic (harmonic.fun)
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.
Endpoint: aristotle.harmonic.fun
Auth: Auth0-based (requires signup/login at harmonic.fun)
| Benchmark | Score |
|---|---|
| MiniF2F | 90% |
| VERINA | 96.8% |
-- 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
sorry
This skill participates in triadic composition:
Skill Name: aristotle-lean Type: Formal Verification / Theorem Proving Trit: -1 (MINUS) GF(3): Conserved in triplet composition
Condition: μ(n) ≠ 0 (Möbius squarefree)
This skill is qualified for non-backtracking geodesic traversal:
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)
npx claudepluginhub plurigrid/asi --plugin asiAssists with Lean 4 theorem proving: editing .lean files, debugging builds (type mismatches, sorries, axioms, lake errors), searching mathlib lemmas, formalizing mathematics, and learning concepts via commands like /lean4:prove and /lean4:formalize.
Provides Lean 4 syntax guide for creating valid `--goal-type` and `--hypotheses` with `./bin/lc create-goal`. Covers function juxtaposition, real constants, set intervals, `;;`-separated hypotheses, and operators.
Generates formal Lean 4 proof state chains using GF(3)-balanced random walks with triad agents (Generator +1, Coordinator 0, Validator -1) for parallel verification. Invoke for theorem proving.