Are there any experts in pure mathematics in this community?
Is there anyone in this community who can issue an arXiv endorsement?
We have completed a formal proof by Coq of the Collatz conjecture.
We are having trouble getting an arXiv endorsement. Can anyone help us?
Axiom R_Definition is absurd.
for example, very rough proof script, someone else feel free to proof golf:
Lemma R_Definition_False : False. Proof. pose proof R_Definition 1 0 as H. assert (0 < 1) as H0 by lia. specialize (H H0). destruct H as [H1 H2]. assert (H3 : Nat.Odd 1) by (exists 0; lia). specialize (H1 H3). lia. Qed.
@Li-yao @Karl Palmskog
Thanks for your quick comment.
Last updated: Sep 23 2023 at 08:01 UTC