Posts

• Oct 23, 2025

  Artificial Algorithms

• Aug 11, 2025

  Thoughts on Informal and Formal Reasoning

• Jul 29, 2025

  Provably-Correct Vibe Coding

• Jul 6, 2025

  Proving Alpha-Beta (Episode 2), Sorry Hammer and More

• 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