Live data from Hacker News

Case study: Creative math – How AI fakes proofs

tomaszmachnik.pl

31–40 of 107 posts

Re: Case study: Creative math – How AI fakes proofs

#31
post #29
post #28

Earlier quoted context omitted.

I remember that being true of early ChatGPT, but it's certainly not true anymore; GPT 4o and 5 have tagged along with me through all of MathAcademy MFII, MFIII, and MFML (this is roughly undergrad Calc 2 and then like half a stat class and 2/3rds of a linear algebra class) and I can't remember it getting anything wrong. Presumably this is all a consequence of better tool call training and better math tool calls behin…

It's definitely gotten considerably better, though I still have issues with it generating proofs, at least with TLAPS. I think behind the scenes it's phoning Wolfram Alpha nowadays for a lot of the numeric and algebraic stuff. For all I know, they might even have an Isabelle instance running for some of the even-more abstract mathematics. I agree that this is largely an early ChatGPT problem though, I just thought it…

I assumed it was just writing SymPy or something.

Re: Case study: Creative math – How AI fakes proofs

#32
post #4
post #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 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)

With a slide rule you can start from 92200 or so, long division with 9.22 gives 9.31 or so, next guess 9.265 is almost on point, where long division says that's off by 39.6 so the next approximation +19.8 is already 92,669.8... yeah the long divisions suck but I think you could get this one within 10 minutes if the interviewer required you to.

Also, don't take a role that interviews like that unless they work on something with the stakes of Apollo 13, haha

Re: Case study: Creative math – How AI fakes proofs

#33
post #32
post #4

Earlier quoted context omitted.

> 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)

With a slide rule you can start from 92200 or so, long division with 9.22 gives 9.31 or so, next guess 9.265 is almost on point, where long division says that's off by 39.6 so the next approximation +19.8 is already 92,669.8... yeah the long divisions suck but I think you could get this one within 10 minutes if the interviewer required you to. Also, don't take a role that interviews like that unless they work on some…

I actually have a slide rule that was my father's in school

great for teaching logarithms

Re: Case study: Creative math – How AI fakes proofs

#34
post #23

I remember when ChatGPT first came out, I asked it for a proof for Fermat's Last Theorem, which it happily gave me. It was fascinating, because it was doing a lot of understandable mistakes that 7th graders make. For example, I don't remember the surrounding context but it decided that you could break `sqrt(x^2 + y^2)` into `sqrt(x^2) + sqrt(y^2) => x + y`. It's interesting because it was one of those "ASSUME FALSE"…

My favorite early chatgpt math problem was "prove there exists infinitely many even primes" . Easy! Take a finite set of even primes, multiply them and add one to get a number with a new even prime factor.

Of course, it's gotten a bit better than this.

Re: Case study: Creative math – How AI fakes proofs

#35
This also can be observed with more advanced math proofs. ChatGPT 5.2 pro is the best public model at math at the moment, but if pushed out of its comfort zone will make simple (and hard to spot) errors like stating an inequality but then applying it in a later step with the inequality reversed (not justified).

Re: Case study: Creative math – How AI fakes proofs

#36
post #23

I remember when ChatGPT first came out, I asked it for a proof for Fermat's Last Theorem, which it happily gave me. It was fascinating, because it was doing a lot of understandable mistakes that 7th graders make. For example, I don't remember the surrounding context but it decided that you could break `sqrt(x^2 + y^2)` into `sqrt(x^2) + sqrt(y^2) => x + y`. It's interesting because it was one of those "ASSUME FALSE"…

LLMs have improved so much the original ChatGPT isn't relevant.

Re: Case study: Creative math – How AI fakes proofs

#38

This 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…

This 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.

Often, if not usually, that means the method should exist.

Re: Case study: Creative math – How AI fakes proofs

#39
post #29
post #28

Earlier quoted context omitted.

I remember that being true of early ChatGPT, but it's certainly not true anymore; GPT 4o and 5 have tagged along with me through all of MathAcademy MFII, MFIII, and MFML (this is roughly undergrad Calc 2 and then like half a stat class and 2/3rds of a linear algebra class) and I can't remember it getting anything wrong. Presumably this is all a consequence of better tool call training and better math tool calls behin…

It's definitely gotten considerably better, though I still have issues with it generating proofs, at least with TLAPS. I think behind the scenes it's phoning Wolfram Alpha nowadays for a lot of the numeric and algebraic stuff. For all I know, they might even have an Isabelle instance running for some of the even-more abstract mathematics. I agree that this is largely an early ChatGPT problem though, I just thought it…

I think behind the scenes it's phoning Wolfram Alpha nowadays for a lot of the numeric and algebraic stuff. For all I know, they might even have an Isabelle instance running for some of the even-more abstract mathematics.

Maybe, but they swear they didn't use external tools on the IMO problem set.

Re: Case study: Creative math – How AI fakes proofs

#40
I like how this article was itself clearly written with the help of an LLM.

(You can particularly tell from the "Conclusions" section. The formatting, where each list item starts with a few-word bolded summary, is already a strong hint, but the real issue is the repetitiveness of the list items. For bonus points there's a "not X, but Y", as well as a dash, albeit not an em dash.)

Post reply on HN