Ciro Santilli @cirosantilli 40

On one hand, formal proof systems prevent hallucinations.

On the other hand, LLMs can handle the mega verbosity and learning curve of formal proof systems which few humans are willing to undertake.

The human only needs to understand the bare minium of the formal proof system to know that statements are what they say they are. LLMs can then take care of the proof entirely.

It's really a killer combo.

Much of this section will be dumped at Section "Website front-end for a mathematical formal proof system" instead.

A proof in some system for the formalization of mathematics.

A theorem that is not very important on its own, often an intermediate step to proving something that the author feels deserves the name "theorem".

Intuitively: unordered container where all the values are unique, just like C++ std::set.

More precisely for set theory formalization of mathematics:

Set of ordered pairs. That's it! This is illustrated at: math.stackexchange.com/questions/1480651/is-fx-x-1-x-2-a-function/1481099#1481099

Most notable example: $L^2$.

An ordered pair of two real numbers with the complex addition and multiplication defined.

Forms both a:

Sets are unordered, but we can use them to create ordered objects, which are of fundamental importance. Notably, they are used in the definition of functions.

This section is about formalization efforts of specific fields of mathematics.