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.

https://figshare.com/collections/The_formal_proof_of_3x_1_problem/6472138

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