Our great sponsors
-
-
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
What solved the problem for me was doing mathematics in a proof assistant. I use Coq, but Lean (which is more popular among mathematicians) works just as well for this purpose. To make a long story short, the proof assistant makes you justify every step in full rigor. There is no distinction between trivial and essential steps. You simply have to do every step. Doing math in a proof assistant gives you the confidence of knowing that, for sure, with 100% certainty, your proof is correct, and you did not skip any steps. (Logically, if you didn't skip any steps at all, then you certainly didn't skip any essential steps.) The foundation that this confidence provides allows you to learn and truly understand ZFC set theory.
What solved the problem for me was doing mathematics in a proof assistant. I use Coq, but Lean (which is more popular among mathematicians) works just as well for this purpose. To make a long story short, the proof assistant makes you justify every step in full rigor. There is no distinction between trivial and essential steps. You simply have to do every step. Doing math in a proof assistant gives you the confidence of knowing that, for sure, with 100% certainty, your proof is correct, and you did not skip any steps. (Logically, if you didn't skip any steps at all, then you certainly didn't skip any essential steps.) The foundation that this confidence provides allows you to learn and truly understand ZFC set theory.