Research-Stack/shared-data/artifacts
Brandon Schneider aa4563cdf5 feat: create Lean Expert Agent with full inspection protocol
Agent inspects Lean code for:
1. Structural health (theorem/def/eval/sorry counts)
2. Naming conventions (camelCase/PascalCase per AGENTS.md)
3. Q0_16/Q16_16 compliance
4. Proof quality (native_decide, .isSome guards, tautologies)
5. Dependency analysis (unused imports, circular deps)

First inspection of Physics/ found 95 issues:
  79 naming violations (systematic snake_case)
  2 unused imports (Semantics.FixedPoint)
  4 trivial/tautological proofs
  3 #eval vs #eval! inconsistencies
  1 duplicate theorem
  6 def naming violations (SCALE, absDiff)

Trigger with: /inspect <target>
2026-05-13 22:01:12 -05:00
..
deepseek_review Correct DeepSeek review receipt attribution 2026-05-11 23:06:57 -05:00
lean_expert_agent feat: create Lean Expert Agent with full inspection protocol 2026-05-13 22:01:12 -05:00