Case study: Creative math – How AI fakes proofs
tomaszmachnik.pl
Case study: Creative math – How AI fakes proofs
1–10 of 107 posts
Re: Case study: Creative math – How AI fakes proofs
#2They can all write lean4 now, don't accept numbers that don't carry proofs. The CAS I use for builds has a coeffect discharge cert in the attestation header, couple lines of code. Graded monads are a snap in CIC.
Re: Case study: Creative math – How AI fakes proofs
#3> a session with Gemini 2.5 Pro (without Code Execution tools)
How good are you at programming on a whiteboard? How good is anybody? With code execution tools withheld from me, I'll freely admit that I'm pretty shit at programming. Hell, I barely remember the syntax in some of the more esoteric, unpracticed places of my knowledge. Thus, it's hard not to see case studies like this as dunking on a blindfolded free throw shooter, and calling it analysis.
Re: Case study: Creative math – How AI fakes proofs
#4> a session with Gemini 2.5 Pro (without Code Execution tools) How good are you at programming on a whiteboard? How good is anybody? With code execution tools withheld from me , I'll freely admit that I'm pretty shit at programming. Hell, I barely remember the syntax in some of the more esoteric, unpracticed places of my knowledge. Thus, it's hard not to see case studies like this as dunking on a blindfolded free thr…
> How good are you at programming on a whiteboard?
pretty good?
I could certainly do a square root
(given enough time, that one would take me a while)
Re: Case study: Creative math – How AI fakes proofs
#5that's not a proof
Re: Case study: Creative math – How AI fakes proofs
#6This is the classic 'plausible hallucination' problem. In my own testing with coding agents, we see this constantly—LLMs will invent a method that sounds correct but doesn't exist in the library.
The only fix is tight verification loops. You can't trust the generative step without a deterministic compilation/execution step immediately following it. The model needs to be punished/corrected by the environment, not just by the prompter.
Re: Case study: Creative math – How AI fakes proofs
#7> a session with Gemini 2.5 Pro (without Code Execution tools) How good are you at programming on a whiteboard? How good is anybody? With code execution tools withheld from me , I'll freely admit that I'm pretty shit at programming. Hell, I barely remember the syntax in some of the more esoteric, unpracticed places of my knowledge. Thus, it's hard not to see case studies like this as dunking on a blindfolded free thr…
It’s like that but if the blindfolded free throw shooter was also the scorekeeper and the referee & told you with complete confidence that the ball went in, when you looked away for a second.
Re: Case study: Creative math – How AI fakes proofs
#8This is the classic 'plausible hallucination' problem. In my own testing with coding agents, we see this constantly—LLMs will invent a method that sounds correct but doesn't exist in the library. The only fix is tight verification loops. You can't trust the generative step without a deterministic compilation/execution step immediately following it. The model needs to be punished/corrected by the environment, not just…
I've been using codex and never had a compile time error by the time it finishes. Maybe add to your agents to run TS compiler, lint and format before he finish and only stop when all passes.
Re: Case study: Creative math – How AI fakes proofs
#9Is this hallucination, or is this actually quite human (albeit a specific type of human)? Think of slimy caricatures like a used car salesman, isn't this the exact type of underhandedness you'd expect?
Re: Case study: Creative math – How AI fakes proofs
#10I am actually surprised that the LLM came so close. I doubt it had examples in its training set for these numbers. This goes to the heart of "know-how". The LLM should should have said: "I am not sure" but instead gets into rhetoric to justify itself. It actually mimics human behavior for motivated reasoning. At orgs, management is impressed with this overconfident motivated reasoner as it mirrors themselves. To hell with the facts, and the truth, persuation is all that matters.