Conversation

LEAN was used to prove the Collatz conjecture. The proof exploited several vulnerabilities in the proving engine, and is not actually valid, which is par for the course for the Collatz conjecture, known exploit of the human mind.

1
0
0

@sophieschmieg relatedly, clang can be used to disprove the collatz conjecture, but is not able to provide a counterexample

0
0
4