/sci/ - Science & Math

In the 19th and 20 century mathematicians worked on formalizing mathematics, and when they achieved results they moved on.
There you have ZFC. Pretty much all mathematics are just these replacement schemes applied again and again. It is unbelievable that we barely use computers to aide us with this.
Yes there exist proof assistants but these are complicated to use and that's why it is rare.
When a new proof is claimed for years it is unsure if it is true.
This shouldn't be the case. What we need is a language that is interpreted into formal logic proofs and theorems.
What I mean by that is that you first of all need a language which allows you to enter proofs as application of axioms or previously proven theorems. This means that you first write down a theorem, and then write a proof into the script using previously proven theorems and the axioms.
The second thing is a program that can check your formal proofs for correct application of axioms (basically trivial)

But the third and modt important thing is commands which allow you to create abstractions at an extreme rate.
We need python or Java and not assembly.
You need to be able to easily define notation and apply previoud theorems.
In the end you can stsrt by formalizing basic set theory, natural numbers and then move on to algebra and analysis.
Formalizing a proof should be no harder than converting pseudocode into python. The mathematicd are settled, the only thing that's missing is an effective language to write it down.

>>10202018
Not an equation, but this comes closest to what you're looking for