4 ms·
Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Formal here is not "Mathy and jargony and
by cscurmudgeon 10y ago
Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics.
Formal here is not "Mathy and jargony and with a lot of greek symbols" as is understood normally.
- jonnybgood 10y ago> Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Right. That's the formal I'm also referring to.
- catnaroek 10y agoMathematical papers are seldom written fully formally. This is in no small part because the most commonly accepted foundation of mathematics (ZFC atop first-order logic) was only designed to make formalization possible “in principle”. It's precisely because of this that researchers in formal verification are looking for systems that make formalization actually possible in practice, such as various flavors of type theory.
- jonnybgood 10y agoGot it. This is what I was missing. Thank you.