Lean4AI @ Gas Station Secret Lab | Using interactive theorem provers like Lean to tackle the great challenges of generative AI: Safety and Hallucination.

Posts

Mar 28, 2025
Property-Based Testing with Dependent Types: Experiment Alpha-Beta
Feb 18, 2025
Hallucination Detection on FVAPPS
Feb 13, 2025
LeanTool: Progress and Roadmap
Feb 5, 2025
Followup on Hallucination Detection and Recovery (progress report #3.5)
Jan 30, 2025
Lean4AI: An Overview
Jan 22, 2025
Hallucination Detection and Recovery: Initial Experiment
Dec 9, 2024
Proving Dynamic Programming with Sonnet (Part 2)
Dec 3, 2024
Proving Memoization in Lean, and Teaching It to Sonnet (Part 1)
Nov 29, 2024
Progress Report #2: FormalizeWithTest, LeanTool
Nov 19, 2024
Progress Report #1: Arena, SafeVerify and More
Nov 4, 2024
A Proposal for Safe and Hallucination-free Coding AI