Is this proof formalization on perfect cuboids correct?

Stream: new members

[Jamal]

I recently developed a simplified and rigorous proof on the non-existence of perfect cuboids as can be found on this GitHub: https://github.com/JAgbanwa/Perfect-Cuboid-Lean-Proof . This is my Lean code : https://github.com/JAgbanwa/Perfect-Cuboid-Lean-Proof/blob/main/Perfect%20Cuboid%20-%20Lean/cuboid.lean.rtf

When I run it on the online Lean website I get this error notification:

MathlibDemo.lean:1:0

object file '/home/lean4web/build/deploy-2025-08-02T18-00-21+00-00/MathlibDemo/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Data/Nat/Prime.olean' of module Mathlib.Data.Nat.Prime does not exist

How do I correct this?

Thanks.

Kind regards.

[Weiyi Wang]

That file is not in the latest version of mathlib, though there is Mathlib.Data.Nat.Prime.Basic and friends. Was this generated by AI? AI can easily output code based on outdated information, and you need to have knowledge on the library itself to correct them

[Weiyi Wang]

(also why is the file extension "rtf"?)

[Eric Wieser]

Why did you keep writing 200 lines of code when there was an error on the second line?

[Notification Bot]

This topic was moved here from #general > Is this proof formalization on perfect cuboids correct? by Eric Wieser.

[Michael Rothgang]

Besides: your message sounded like it was a complete proof --- but your file has 9 sorries, which appear to be significant work. Asking for help on in-progress work is fine! However, please be careful with making claims "it's done" when it clearly is not.

[Michael Rothgang]

(There have been a number of posts of the kind "I have a complete proof of <something complicated>", with the Lean code appearing AI generated and of rather bad quality. I personally don't have much patience for this left. If you use AI, please be very careful what you're claiming.)

[Michael Rothgang]

Also: if I understand correctly, the perfect cuboid problem is an open problem in mathematics. If you believe you have a new and short solution (that nobody found yet), that's all the more reason to be careful and skeptical of your work.

[Jamal]

Michael Rothgang said:

Besides: your message sounded like it was a complete proof --- but your file has 9 sorries, which appear to be significant work. Asking for help on in-progress work is fine! However, please be careful with making claims "it's done" when it clearly is not.

Thanks for your feedback. I tried to address a full proof, but it is still in-progress. I would also be glad to receive feedback and help correcting these sorry's too.

[Jamal]

Michael Rothgang said:

Also: if I understand correctly, the perfect cuboid problem is an open problem in mathematics. If you believe you have a new and short solution (that nobody found yet), that's all the more reason to be careful and skeptical of your work.

Honestly the Lean code is AI generated I have only began to learn it. I was only inspired to try using AI to generating Lean codes to see how that works here from this video: https://www.youtube.com/watch?v=zZr54G7ec7A&t=1057s ,which was why I tried this out. I would also appreciate assistance with making correct my code if possible.

[Ruben Van de Velde]

There is no point in asking a computer to generate code you don't understand yourself. If you want to learn lean, there's a number of learning resources linked from the website, but there's no shortcut to learning the language yourself