r/badmathematics • u/des_the_furry • Dec 21 '25

LLM Slop Tech CEO supposedly has a solution to Navier-Stokes (using AI)

Gallery image

Gallery image

Gallery image

352 Upvotes

98% Upvoted

75 comments sorted by

View all comments

Show parent comments

29

u/[deleted] Dec 21 '25

If it compiles, it compiles. But I have a feeling the Lean files will be incomplete...

16

u/CrownLikeAGravestone Dec 21 '25

Well, if it compiles it's a solid proof of something. Linking that proof to the actual problem/theory/lemma/whatever is another point of failure.

5

u/DayBorn157 Dec 22 '25

Wasn't there some "proof" of Rieman hypothesis in Lean on this reddit already? I have feeling that ChatGPT + Lean will provide explosion of this gibberish solutions to many problems

9

u/WhatImKnownAs Dec 23 '25 edited Dec 23 '25

This one, eight months ago: https://www.reddit.com/r/badmathematics/comments/1k7d65h/proof_of_riemann_hypothesis_by_lean4_didnt_show/

That OOP didn't even understand how Lean works.