GasStationManager
@gasstationmanager.bsky.social
Independent AI Researcher.
Blogging at https://gasstationmanager.github.io/
Building stuff at https://github.com/GasStationManager
Blogging at https://gasstationmanager.github.io/
Building stuff at https://github.com/GasStationManager
Pinned
A Proposal for Safe and Hallucination-free Coding AI
Update 11/19: First progress report.
gasstationmanager.github.io
My essay on making coding AIs safe and hallucination-free gasstationmanager.github.io/ai/2024/11/0...
#LLM #AISafety #blueskAI
#LLM #AISafety #blueskAI
gasstationmanager.github.io/ai/2025/03/2...
Work in progress; comments welcome!
Work in progress; comments welcome!
Property-Based Testing with Dependent Types: Experiment Alpha-Beta
(This also serves as progress report #4 of our overall program.)
gasstationmanager.github.io
April 11, 2025 at 12:00 PM
gasstationmanager.github.io/ai/2025/03/2...
Work in progress; comments welcome!
Work in progress; comments welcome!
LeanTool github.com/GasStationMa...
Now supports Sonnet 3.7; also available as a model-context-protocol (MCP) server that can be plugged into Claude Code.
Now supports Sonnet 3.7; also available as a model-context-protocol (MCP) server that can be plugged into Claude Code.
GitHub - GasStationManager/LeanTool: A "code intepreter" for Lean
A "code intepreter" for Lean. Contribute to GasStationManager/LeanTool development by creating an account on GitHub.
github.com
February 26, 2025 at 6:03 PM
LeanTool github.com/GasStationMa...
Now supports Sonnet 3.7; also available as a model-context-protocol (MCP) server that can be plugged into Claude Code.
Now supports Sonnet 3.7; also available as a model-context-protocol (MCP) server that can be plugged into Claude Code.
A couple updates to LeanTool github.com/GasStationMa... : Now supporting reasoning models like o3-mini and r1; also with a demo proxy server up at the base URL www.codeproofarena.com:8800/v1
www.codeproofarena.com
February 15, 2025 at 7:58 PM
A couple updates to LeanTool github.com/GasStationMa... : Now supporting reasoning models like o3-mini and r1; also with a demo proxy server up at the base URL www.codeproofarena.com:8800/v1
More results from my hallucination detection and recovery experiments:
gasstationmanager.github.io/ai/2025/02/0...
Try your favorite model/prompt/reasoning strategy on these!
gasstationmanager.github.io/ai/2025/02/0...
Try your favorite model/prompt/reasoning strategy on these!
Followup on Hallucination Detection and Recovery (progress report #3.5)
In this followup update to my initial experiment, I report on some additional results as I apply the same approach to more problem instances.
gasstationmanager.github.io
February 5, 2025 at 7:43 PM
More results from my hallucination detection and recovery experiments:
gasstationmanager.github.io/ai/2025/02/0...
Try your favorite model/prompt/reasoning strategy on these!
gasstationmanager.github.io/ai/2025/02/0...
Try your favorite model/prompt/reasoning strategy on these!
Lean4AI Reading Guide: gasstationmanager.github.io/ai/2025/01/3...
January 30, 2025 at 8:42 PM
Lean4AI Reading Guide: gasstationmanager.github.io/ai/2025/01/3...
How to detect hallucinations in the output of coding AI models? My approach is to utilize interactive theorem provers like Lean. See my blog post for details: gasstationmanager.github.io/ai/2025/01/2...
#lean #leanprover #ai
#lean #leanprover #ai
Hallucination Detection and Recovery: Initial Experiment
(This also serves as progress report #3 of our overall program)
gasstationmanager.github.io
January 22, 2025 at 11:23 PM
How to detect hallucinations in the output of coding AI models? My approach is to utilize interactive theorem provers like Lean. See my blog post for details: gasstationmanager.github.io/ai/2025/01/2...
#lean #leanprover #ai
#lean #leanprover #ai
github.com/GasStationMa...
Connects LLMs with a "code interpreter" for Lean. Here's a proof Sonnet did in a recent chat session.
Connects LLMs with a "code interpreter" for Lean. Here's a proof Sonnet did in a recent chat session.
December 17, 2024 at 6:13 AM
github.com/GasStationMa...
Connects LLMs with a "code interpreter" for Lean. Here's a proof Sonnet did in a recent chat session.
Connects LLMs with a "code interpreter" for Lean. Here's a proof Sonnet did in a recent chat session.
gasstationmanager.github.io/ai/2024/12/0...
I asked Claude Sonnet to prove the correctness of dynamic programming in Lean
I asked Claude Sonnet to prove the correctness of dynamic programming in Lean
Proving Dynamic Programming with Sonnet (Part 2)
This is Part 2 of a series where I explore techniques for proving correctness of algorithms in Lean, and then teaching it to Claude Sonnet. You may want to start with Part 1 on memoization.
gasstationmanager.github.io
December 11, 2024 at 7:42 AM
gasstationmanager.github.io/ai/2024/12/0...
I asked Claude Sonnet to prove the correctness of dynamic programming in Lean
I asked Claude Sonnet to prove the correctness of dynamic programming in Lean
Code with Proofs Benchmark. Now on Huggingface.
huggingface.co/datasets/Gas...
huggingface.co/datasets/Gas...
GasStationManager/CodeProofBenchmark · Datasets at Hugging Face
We’re on a journey to advance and democratize artificial intelligence through open source and open science.
huggingface.co
December 8, 2024 at 11:18 PM
Code with Proofs Benchmark. Now on Huggingface.
huggingface.co/datasets/Gas...
huggingface.co/datasets/Gas...
Once your model reach the top and you attract enough funding to acquire compute, then it is the time to modify your approach to make sure it scales. That is by no means easy, but I believe it is the best response. (2/2)
Here's my hot take on the bitter lesson. It is very likely true, but it only holds in the long term. That's why OpenAI people love to recommend it, because following it ensures whoever has the most compute dominates. And that is why for anyone else, now is the time to try novel ideas. (1/2)
#ai
#ai
Thoughts on Richard Sutton's 'bitter lesson'?
"... the actual contents of minds are tremendously, irredeemably complex; we should stop trying to find simple ways to think about the contents of minds..."
Okay (maybe?) for engineering but not understanding.
www.incompleteideas.net/IncIdeas/Bit...
"... the actual contents of minds are tremendously, irredeemably complex; we should stop trying to find simple ways to think about the contents of minds..."
Okay (maybe?) for engineering but not understanding.
www.incompleteideas.net/IncIdeas/Bit...
December 6, 2024 at 6:24 PM
Once your model reach the top and you attract enough funding to acquire compute, then it is the time to modify your approach to make sure it scales. That is by no means easy, but I believe it is the best response. (2/2)
Here's my hot take on the bitter lesson. It is very likely true, but it only holds in the long term. That's why OpenAI people love to recommend it, because following it ensures whoever has the most compute dominates. And that is why for anyone else, now is the time to try novel ideas. (1/2)
#ai
#ai
Thoughts on Richard Sutton's 'bitter lesson'?
"... the actual contents of minds are tremendously, irredeemably complex; we should stop trying to find simple ways to think about the contents of minds..."
Okay (maybe?) for engineering but not understanding.
www.incompleteideas.net/IncIdeas/Bit...
"... the actual contents of minds are tremendously, irredeemably complex; we should stop trying to find simple ways to think about the contents of minds..."
Okay (maybe?) for engineering but not understanding.
www.incompleteideas.net/IncIdeas/Bit...
The Bitter Lesson
www.incompleteideas.net
December 6, 2024 at 6:18 PM
Here's my hot take on the bitter lesson. It is very likely true, but it only holds in the long term. That's why OpenAI people love to recommend it, because following it ensures whoever has the most compute dominates. And that is why for anyone else, now is the time to try novel ideas. (1/2)
#ai
#ai
gasstationmanager.github.io/ai/2024/12/0...
The prettiest piece of #lean code I have written. After which I taught Sonnet how to do it.
The prettiest piece of #lean code I have written. After which I taught Sonnet how to do it.
Proving Memoization in Lean, and Teaching It to Sonnet (Part 1)
Consider memoization. This is a very general algorithmic technique: given a recursive function, we use a map-like data structure to cache its return values so that later calls can directly look up the...
gasstationmanager.github.io
December 4, 2024 at 12:31 PM
gasstationmanager.github.io/ai/2024/12/0...
The prettiest piece of #lean code I have written. After which I taught Sonnet how to do it.
The prettiest piece of #lean code I have written. After which I taught Sonnet how to do it.
Just found out about this project. Very cool!
Pantograph, a #lean4 tool designed for training and evaluating neural theorem provers, has been released. It supports incremental tactic execution and proof drafting: arxiv.org/abs/2410.16429
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a surge of interest in us...
arxiv.org
December 2, 2024 at 7:13 AM
Just found out about this project. Very cool!
Reposted by GasStationManager
November 30, 2024 at 12:14 AM
github.com/GasStationMa...
My repository with proof of concept and some preliminary results on autoformalization of coding problems.
My repository with proof of concept and some preliminary results on autoformalization of coding problems.
GitHub - GasStationManager/FormalizeWithTest: Autoformalization of coding problems, verified with test cases
Autoformalization of coding problems, verified with test cases - GasStationManager/FormalizeWithTest
github.com
November 29, 2024 at 3:34 AM
github.com/GasStationMa...
My repository with proof of concept and some preliminary results on autoformalization of coding problems.
My repository with proof of concept and some preliminary results on autoformalization of coding problems.
November 28, 2024 at 8:36 PM
Reposted by GasStationManager
Any Lean enthusiasts here? You might be interested in Code with Proofs: the Arena www.codeproofarena.com:8000
Test your Lean 4 skills with our coding challenges!
#lean
Test your Lean 4 skills with our coding challenges!
#lean
www.codeproofarena.com
November 25, 2024 at 10:15 PM
Any Lean enthusiasts here? You might be interested in Code with Proofs: the Arena www.codeproofarena.com:8000
Test your Lean 4 skills with our coding challenges!
#lean
Test your Lean 4 skills with our coding challenges!
#lean
My essay on making coding AIs safe and hallucination-free gasstationmanager.github.io/ai/2024/11/0...
#LLM #AISafety #blueskAI
#LLM #AISafety #blueskAI
A Proposal for Safe and Hallucination-free Coding AI
Update 11/19: First progress report.
gasstationmanager.github.io
November 24, 2024 at 2:07 PM
My essay on making coding AIs safe and hallucination-free gasstationmanager.github.io/ai/2024/11/0...
#LLM #AISafety #blueskAI
#LLM #AISafety #blueskAI