Lean4AI @ Gas Station Secret Lab
About

Posts

  • Jun 8, 2025

    Proving Alpha-Beta, Episode 1

  • May 22, 2025

    Alpha-Beta with Goose + Gemini

  • May 15, 2025

    Alpha-Beta with Claude Code

  • 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

subscribe via RSS

Lean4AI @ Gas Station Secret Lab

  • Lean4AI @ Gas Station Secret Lab
  • GasStationCodeManager@gmail.com
  • GasStationManager

Using interactive theorem provers like Lean to tackle the great challenges of generative AI: Safety and Hallucination.