Goals and Roadmap for the Physics Derivation Graph

navigation / documentation overview / Goals and Roadmap

Content:

1. enter a derivation
2. enter a derivation per major domain
3. enter derivations that span 2 domains
4. identify derivations that connect the above

Validation: In a CAS, and then in Lean,

1. Validate an expression
2. Validate a step
3. Validate the majority of steps and expressions in a derivation
4. Validate all steps and expressions in a derivation
5. Validate an expression and step from each derivation
6. Validate the majority of steps and expressions in every derivation
7. Validate all steps and expressions in all derivations

Demonstrate all the proposed queries.

1. Demonstrate use in an arxiv paper
2. Demonstrate the cross reference in 2 published papers

Definition of done is when the following conditions are met:

• There is an expression associated with every domain of physics
  and
• Every expression is part of a derivation
  and
• Every derivation is connected to one or more other derivations
  and
• Every step in a derivation is proven using lean
  and
• There is a connection from any derivation to every other derivation