npx claudepluginhub plurigrid/asi --plugin asiThis skill uses the workspace's default tool permissions.
**Trit**: -1 (MINUS)
Assists 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.
Share bugs, ideas, or general feedback.
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)