Roadmap for Formal Mathematical Physics Content


Explanation: Here the focus is on a single inference rule and verifying the inference rule with respect to a logical basis like Zermelo–Fraenkel set theory in a formal proof assistent like Coq or Lean.

This validation per inference rule would need to be applied to each inference rule used in the derivation.

Who does this work: human content creator

Motive for doing this work:

  1. lecture video
  2. hand-written notes
  3. Latex document
  4. Content tags
  5. tags for sections and words and expressions
  6. concepts to variables
  7. all steps
  8. derivation graph
  9. replace symbols with numeric ID
  10. validation of steps
  11. validation of dimension
  12. proof of inference rule
Back to layers overview

The expression \begin{equation} \frac{1}{2} m_1 v^2 = \frac{G m_1 m_2}{r} \label{eq:initial} \end{equation} reduces to \begin{equation} v^2 = \frac{2Gm_2}{r} \end{equation} when both sides of Eq.~\ref{eq:initial} are multiplied by $$2/m_2$$

(Insert proof of "multiply both sides by" here)