yamafaktory/formal
A Lean 4 + Mathlib proof service for the agent working on your code
4 best points · 4 comments · 3 Hacker News posts · 25 GitHub stars · View on GitHub
Hacker News discussions
- Show HN: Formal – Formal verification for AI-generated code using Lean 4 (4 points, 4 comments, by yamafaktory, 2026-04-12)
- Show HN: Formal – LLM-driven property checker, backed by Lean 4 and Mathlib (1 points, 0 comments, by yamafaktory, 2026-04-13)
- Show HN: Formal – LLM-driven property checker backed by Lean 4 and Mathlib (1 points, 0 comments, by yamafaktory, 2026-04-16)