Physics Derivation Graph navigation Sign in

degrees of formalization in math

Published 2020-07-30T14:22:00.002Z by Physics Derivation Graph

Update 2021-07-30: this concept is the de Bruijn factor.

There are many different views of formalization for mathematics. They are not all competing in the same scope. There are different degrees of formalization. Three analogies for this are
The idea of "zooming visualization" is relevant to the user experience -- a reader should be able to select the level of granularity.

The idea of "compiling" is about making implicit concepts explicit. Also, compiling to different architectures is similar to formalizing in different logics and axioms. Unlike the visualization concept, there is not one underlying basis to specify formalization in.

What are the degrees of formalization in math?
  1. verbal (hallway chats, post-conference dinners, coffee breaks)
  2. white board or chalk board
  3. physical paper + pen or pencil
  4. typesetting: Latex or equivalents like Markdown or (XML based) or pandoc; Powerpoint; Rmd, reStructuredText, MyST, jupyterbook
  5. semantic enrichment/decoration: sTeX, OMDoc; PDG inference rules; pf2 package (sty)
  6. controlled natural languages (e.g., Naproche)
  7. CAS verification of inference rules (e.g. Sage, SymPy)
  8. formal verification in a selected target logic and axioms (e.g., Lean, Isabella, COQ)

References and