Stream: Coq users

Topic: Collatz conjecture

view this post on Zulip Teruyuki Kobayashi (Mar 17 2023 at 10:40):

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?

view this post on Zulip Li-yao (Mar 17 2023 at 10:45):

Axiom R_Definition is absurd.

view this post on Zulip Karl Palmskog (Mar 17 2023 at 11:12):

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.

view this post on Zulip Teruyuki Kobayashi (Mar 17 2023 at 11:33):

@Li-yao @Karl Palmskog
Thanks for your quick comment.

Last updated: Oct 13 2024 at 01:02 UTC