Hideaki Takahashi·2d agoBuilding a Mini Lean 4 from Scratch: Implementing an Interactive Theorem Prover in RustEveryone is talking about interactive theorem provers like Lean 4 and Coq right now. From formalizing frontier mathematics to verifying…
Volodymyr Pavlyshyn·6d agoCertified answers for knowledge graphsLeanRDF puts RDF entailment in Lean 4: Elpi searches, a verified checker decides, and every “yes” comes with a theorem.
Hideaki Takahashi·Oct 29I Rebuilt an AI Gateway in Rust. It Became 41× Faster.Reimplementing LiteLLM with Rust with h5i-app, optimizing streaming and database operations, and formally verifying core logic with Lean 4.
Volodymyr Pavlyshyn·Oct 28Your Agent’s Memory Should Be Able to Say NoA user tells your assistant: Anna and Lena met in Berlin on day 2001, from 10:00 to 12:00. The model turns the sentence into a fact and…
Volodymyr Pavlyshyn·Oct 27Bulletproof Agent with Verifiable Certified OntologiesMost ontologies are described, not proved: OWL and SHACL tell you what a reasoner believes, but they do not hand you a certificate that you…
Hideaki Takahashi·Oct 19I Tried to Formally Verify Popular Rust Projects with Lean 4, but Found More Bugs Than I ExpectedI tried building a benchmark for formally verifying popular Rust OSS. Along the way, I ended up finding real security vulnerabilities.
Hideaki Takahashi·Oct 6Proving Rust Web Application Correctness with Lean 4AI coding agents such as Claude Code and Codex are making it possible to build surprisingly large web applications in a very short amount…A response icon1A response icon1
AI Assurance , Inc.·Oct 4Responsibility OS × EU AI Act — A Lean 4 Reference Model for Preserving Responsibility EvidenceThe EU AI Act (Regulation (EU) 2024/1689) introduces a wide range of requirements for high-risk AI systems, including technical…
Proof Press·Sep 27Applied Identity Physics: Formally Verified Reduction of Holographic Gravity to the Noble Boundary…-- ============================================================
