3 ms·
> 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 referr
by 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.