A proof in some system for the formalization of mathematics.
The only cases where formal proof of theorems seem to have had actual mathematical value is for theorems that require checking a very large number of case, so much so that no human can be fully certain that no mistakes were made. Some examples:
One of the first formal proof systems. This is actually understandable!
This is Ciro Santilli-2020 definition of the foundation of mathematics (and the only one he had any patience to study at all).
TODO what are its limitations? Why were other systems created?
It seems to implement Zermelo-Fraenkel set theory.
A set of axioms is consistent if they don't lead to any contradictions.
When a set of axioms is not consistent, false can be proven, and then everything is true, making the set of axioms useless.
A theorem is said to be independent from a set of axioms if it cannot be proven neither true nor false from those axioms.
It or its negation could therefore be arbitrarily added to the set of axioms.
A conjecture is an open problem in mathematics for which some famous dude gave heuristic arguments which indicate if the theorem is true or false.
This section groups conjectures that are famous, solved or unsolved.
They are usually conjectures that have a strong intuitive reasoning, but took a very long time to prove, despite great efforts.
Given stuff like arxiv.org/pdf/2107.12475.pdf on Erdős' conjecture on powers of 2, it feels like this one will be somewhere close to computer science/Halting problem issues than number theory. Who knows. This is suggested e.g. at The Busy Beaver Competition: a historical survey by Pascal Michel.
We ust use the if mod notation definition as mentioned at: math.stackexchange.com/questions/4305972/what-exactly-is-a-collatz-like-problem/4773230#4773230
Described at: arxiv.org/pdf/2107.12475.pdf where a relation to the Busy beaver scale is proven, and the intuitive relation to the Collatz conjecture described. Perhaps more directly: demonstrations.wolfram.com/CollatzSequenceComputedByATuringMachine/
An easy to prove theorem that follows from a harder to prove theorem.
