Skip to content

Latest commit

 

History

1,538 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

In mathematical physics there are phrases that have specific meanings:

  • Trivial: The instructor knows the answer and assumes you should too.
  • Obvious: The instructor has seen the proof before, but can't remember it right now.
  • Non-trivial: The instructor doesn't know the answer.
  • Left as an exercise to the reader: The instructor doesn't know how to solve it.

If you've read a scientific paper or textbook and wondered how the author jumped from one mathematical observation to another, this project is for you.

The Physics Derivation Graph project makes the "trivial" explicit

The Physics Derivation Graph provides a web server for building, managing, and exploring mathematical derivations in physics (and potentially other fields). The Physics Derivation Graph is an interface for knowledge management software tailored for structured mathematical reasoning. The intended audience includes physicists, mathematicians, and other researchers who need to create, manage, and validate derivations. For additional documentation see https://allofphysics.com/documentation/overview

The questions motivating this project are

  1. Is every expression in physics related to all other expressions in physics?
  2. Naively the expected answer is yes, but then how are expressions in physics related? (The concept of "expression" includes equations and inequalities.)

A claim to validate is that a directed graph exists which describes all of mathematical Physics.

There are a couple consequences of framing mathematical physics expressions as a directed graph:

  • This graph-centric approach to expressions does not include geometric aspects of physics. Force diagrams, optics diagrams, electromagnetic diagrams are not in scope.
  • Inference rules (the things that connect expressions in the form of a derivation step) can be a subject of study.

One could stop the analysis at this point. Or another question might be tempting:
3) could the analysis be done using a computer?
A second claim could be evaluated: the graph representation of mathematical physics is machine parsable.

The Physics Derivation Graph is software that supports investigation of how and whether expressions in mathematical physics are related.

Once a computer is introduced, new questions arise:
4) Can steps be checked?
5) How formal can the check be?

Machine-parsable representations of mathematical physics can be checked by a Computer Algebra Systems (CAS). Steps involving an inference rule and two or more expressions could be checked using Lean Theorem Prover.

This repo is an evolution from previous attempts to investigate the above questions. This repo (which is the code used for https://allofphysics.com/) contains a new web interface, new APIs, and a new backend: Neo4j property graph. The previous version of PDG is https://github.com/allofphysicsgraph/ui_v7_website_flask_json.

In the context of the Physics Derivation Graph, "contributor" can refer to a few different aspects. Contributing derivations or accessing existing derivations is being user; see allofphysics.com/documentation/user and use the web interface or API for allofphysics.com. Another from of being a contributor can refer to modifying the backend source code and evaluating the changes; this requires running a local instance of the project. The rest of this README is aimed at folks interested in running a local instance of the project.

Status

The website and back-end work. Some APIs are operational. The Docker images in this repo are used for https://allofphysics.com/.

Quickstart to Run the Server

Normal users access https://allofphysics.com/ to view and update the Physics Derivation Graph. If you're looking to alter the back-end source code (e.g., Neo4j), front-end source code (web UI, API), or restructure the documentation, then you'll need to review those changes by running an instance of the web server locally.

Launching locally will require generating the certificates for https. See certs/README.md

Assuming Docker is running, to start the containers use

make container_build
make launch_webserver

and then, in a web browser, go to http://localhost

Some pages require Google authentication. To configure this for running your webserver locally you can either

Because software is in Docker containers (for reproducibility), the versions of the Docker software you're using matter. The software in this repo has been tested with

  • docker compose version yields "2.34.0-desktop.1" on a Mac Airbook arm64; "v2.2.1" on a Mac Airbook amd64
  • Compose file format 3.6
  • docker --version yields "Docker version 28.0.4, build b8034c0" on a Mac Airbook arm64; "Docker version 20.10.11" on a Mac Airbook amd64 See https://docs.docker.com/compose/compose-file/compose-versioning/ for compatibility of versions.

Quickstart on the VPS (Virtual Private Server)

make launch_webserver COMPOSE_FLAGS=--detach

and to stop

make down

Project contents

Three containers are managed using docker compose: Neo4j (port 7474), nginx, and a Flask-based Python web server (port 5000).

For more guidance on where various project files are and the relations among dependencies see allofphysics.com/documentation/developer.

Neo4j for newbies

A graph has "nodes" and "edges". A property graph extends that data structure to allow "properties" for both the nodes and the edges.

In general, nodes in Neo4j are described using the following jargon:

:label {key1:'value1', key2:'value2'}

where the key-value pairs are properties.

For examples of queries, see https://allofphysics.com/query

Node labels, relationship types, and properties (the key part) are case sensitive. citation

Goals

  • Document Derivations. Provide a structured way to represent mathematical derivations by breaking them into steps, expressions, and symbols.
  • Facilitate Collaboration and Sharing by using open source and publicly accessible information.
  • Enable programmatic interaction with the data using both a web interface and API.
  • Demonstrate use of SymPy to validate dimensional consistency of expressions.
  • Demonstrate use of SymPy to validate derivation steps.
  • Check a step using Lean Theorem Prover.
  • Validate the claim that all expressions in mathematical physics are related by a finite number of inference rules.
  • Determine what inference rules are necesssary to document all derivations in mathematical physics.

Licensing

The content of this repo is covered by the Creative Commons Attribution 4.0 International License

Software Requirements

Software has been run on Mac and Linux.

  • Docker containers
  • git version control
  • make for building software
  • a web browser to view HTML pages.

Key features

The architecture is Neo4j-Flask-Gunicorn-Nginx all inside a Docker container on an Ubuntu VPS that includes UFW.

The Docker images include the software needed for the webserver (Python Flask):

  • Latex for rendering equations as PNG and PDF
  • SymPy for validating steps in derivations
  • Lean for Theorm Proving
  • Graphviz for static visualization of graphs
  • d3js for interactive visualizations of graphs

See VERSIONS.md for details.

Debugging

The Makefile contains targets that are relevant for validating modifications:

  • make black_out checks formatting and syntax
  • make mypy_out check type hints
  • make pytest_out runs tests

To enter the container for debugging purposes,

docker exec -it `docker ps | grep ui_v8_website_flask_neo4j_webserver | cut -d' ' -f1` /bin/bash

Stuck? Contact the author for help! (See the bottom of https://allofphysics.com/ and the "contact" link.)

Contributing

See CONTRIBUTING.md in this repo for guidance.

Why

The "why" for this project of documenting mathematical physics is merely intellectual curiosity. There's no competition, no leaderboard, and no potential for profit. The author of this project gets to be a dilettante!

Benefits

  • Specifying symbols and operations used in expressions ensures clarity to readers of the author's intent. (No more "what is x?")
  • Formalization can reduce the incidence of mistakes in derivations using rigorous mathematical validation.
  • There is educational value in explicitly identifying the inference rules and assumptions for a derivation.

#EOF

About

version 8 of the Physics Derivation Graph UI: a flask-based website with Neo4j property graph backend

Topics

Resources

Contributing

Stars

2 stars

Watchers

2 watching

Forks

Releases

Sponsor this project

Packages

Used by

Contributors

Languages