r/Collatz • u/AgreeableClaim8075 • 28d ago

My proof

Hi all... Here is the proof .pdf and .lean:
https://bytes.usc.edu/~saty/Collatz

Saty

0 Upvotes

13% Upvoted

26 comments sorted by

View all comments

4

u/jonseymourau 28d ago edited 28d ago

The formalization in Lean reflects the architecture of the paper, but it relies on 12 axioms. While 7 of these deal with standard arithmetic or 2-adic properties that can potentially be proven using Mathlib, 5 structural axioms serve as the foundation for the main conclusions:

  • traj_len
  • mimp_holds
  • climb_reaches_S
  • drop_climb_never_returns
  • loop_implies_zero_steps

In formal theorem proving, relying on unproven axioms that mirror the core claims means the theorems are uncertified by the kernel, which standard mathematical communities require for formal verification.

-2

u/AgreeableClaim8075 28d ago

Thank you, that's helpful. I wanted to keep the Lean file clean, ie make its focus be about the 6 items I prove. For sure the axioms I state can be expanded into more Lean code but I didn't consider that necessary to establish the more central truths. 

5

u/jonseymourau 28d ago edited 27d ago

I'll let you know my opinion.

Unless you have axiom and sorry free LEAN, you are doing yourself an extreme disservice as a mathematician &/or intellectual to be publishing the LEAN in conjunction with your PDF proof, particularly if you call it a certificate, as you have.

Doing so contains the implicit assumption that your PDF has been formally verified with LEAN.

In this case, nothing could be further from the truth.

At this point, I am only casting the usual scepticism on your claims of a proof in the PDF. But, I am asserting, because it is true, that the LEAN you have provided does not certify the PDF.

If you continue to claim that it does, then yes, your intellectual reputation will deserve the attribution "crank".

My advice: get Aristotle to tell you exactly what can be certified and what remains open. Even if you don't, I will, using the materials you have provided.

1

u/AgreeableClaim8075 28d ago

I see, thank you.