What if an AI solving a physics problem had to leave behind more than a convincing explanation? What if it had to leave code, assumptions, source references, tests, and an honest record of what remains unknown?
AI can explain physics beautifully. It can also confidently skip a condition, invent a mathematical operation, solve a subtly different problem, or mistake a plausible hypothesis for a scientific result. Better prompts help, but prompts alone are not a research infrastructure.
That is the problem the Phys infrastructure project is trying to address: give humans, physicists, and AI agents a shared, inspectable framework for representing physics, expressing assumptions, checking supported mathematical steps, and testing the code that carries those steps out.
The goal is not to claim that AI can automatically discover the laws of Nature. It is to make AI-assisted exploration more rigorous—and to make it easier to tell the difference between a good idea, a valid derivation, and a claim supported by physical evidence.
The real problem is bigger than hallucination
“Garbage in, garbage out” is often treated as a data-quality problem. In research, the garbage can enter much earlier than the calculation.
An agent may misunderstand the paper, use the wrong convention, omit a boundary condition, confuse an assumption with a conclusion, or formalize a claim that is easier to prove but no longer means what the researcher intended. A theorem prover can then verify a proof of the wrong proposition. Conversely, even a perfectly specified problem can be ruined by an invalid derivation or faulty implementation.
A trustworthy workflow must therefore distinguish at least five questions:
- Is this the right question? Is the problem meaningful and scoped to a clear regime?
- Did we capture the source correctly? Are the definitions, assumptions, equations, and limitations faithful to the paper or textbook?
- Is the mathematical model appropriate? Does it express the physical idea we intend to study?
- Does the result follow? Were the operations actually performed and checked?
- Does the model describe Nature? Is there relevant empirical evidence—or is that still unknown?
No single test can answer all five. A source citation does not prove an equation. A passing unit test does not validate a physical theory. A replayed derivation does not establish empirical truth. And a formal proof only concerns the proposition and foundations that were actually supplied.
Phys aims to make these distinctions visible, structured, and testable instead of burying them in an AI-generated paragraph.
Why Go—and why code the solution?
Phys is being developed in Go. That is not because physics can be reduced to software, or because every equation can already be executed by the current libraries. It is because a Go project can make supported parts of a solution concrete: typed representations, explicit operations, reproducible test commands, dependency versions, and automated checks in one workflow.
Instead of accepting only a natural-language answer, a physics task can produce an inspectable research package: a problem statement, a source reference, declared assumptions, equations or derivation artifacts, tests for the supported steps, and a report that names unsupported work. The specification should be executable where it can be given precise machine-checkable meaning; interpretive or unresolved claims must remain explicit rather than being disguised as passing tests.
This changes the evaluation question from “Does the AI sound right?” to “What did it represent, what code ran, what did the tests establish, and what did it leave unverified?”
The layers of Phys
The project separates responsibilities that are easy to conflate:
- PhysArtifact provides canonical artifact identity and encoding. It helps identify which exact object is referenced; identity is not proof of correctness.
- PhysMath provides theory-neutral mathematical representations and a bounded set of implemented symbolic operations. It is not a universal computer algebra system or a numerical solver.
-
PhysLib holds physical-framework-specific assumptions, equations, and semantics in
phys-*packages. GR concepts should not be forced onto quantum mechanics or another framework just because an API is convenient. - PhysTrace provides the derivation-specification guidance and workflow discipline: source mapping, capability audits, independent expected results, tests, provenance, and honest evidence levels.
The architecture intentionally separates the mathematical object from its physical interpretation, and both from evidence about the real world. Current capabilities must be checked against the code and executable rule registry—not inferred from a README or an attractive API name.
Math Reality Check: mathematics is the bridge, not the verdict
Link: MRC in markdown, MRC in pdf
The role of mathematics in physics is more subtle than “write an equation, then solve it.” Mathematics lets us make assumptions precise, derive consequences, expose internal contradictions, compare candidate models, and generate predictions that may be confronted with observation. It can reveal that a hypothesis has an impossible consequence under its own assumptions—or that several ideas which sound different share the same mathematical structure.
But mathematical consistency does not automatically make a hypothesis physically true. A model can be internally coherent and still fail to describe Nature. Conversely, an unfamiliar model should not be rejected merely because its notation looks strange; the relevant question is what its assumptions imply and whether those implications are coherent and empirically adequate.
This is the purpose of a Math Reality Check (MRC) in the Phys research vision: turn a hypothesis into concrete, checkable theoretical scenarios. State the assumptions and equations, derive the result, compare it with a clearly defined null model, and record the outcome. Where the problem admits a formal calculation, compute the result from the declared mathematics rather than relying on verbal plausibility. Where there is no empirical evidence, the Nature/Reality outcome remains UNOBSERVED or NOT AVAILABLE—not silently marked as confirmed.
MRC is not a machine that declares a Theory of Everything true. It is a discipline for asking what a hypothesis actually commits us to, what it predicts, which competing or null model it beats or fails to beat, and what evidence would change our minds.
That discipline should shape hypothesis formulation from the beginning. An AI agent should not merely invent an elegant equation and then defend it. It should list the assumptions, identify the regime, search for counterexamples, derive distinguishing predictions where possible, compare alternatives, and say what would falsify or constrain the idea.
Phys and Lean: complementary, not competing
Lean is an interactive theorem prover and programming language. Its kernel checks proof terms against formal propositions and their definitions and assumptions. Mathlib supplies a large reusable library of formal mathematics. These are powerful tools for asking whether a precise mathematical statement follows from declared foundations.
Phys is concerned with a different—but connected—part of the pipeline: did we formulate the right claim in the first place, preserve its physical assumptions and source meaning, and record what the derivation actually establishes?
A useful shorthand is:
- Phys helps make the research inputs explicit and auditable. What is the source claim? Which assumptions and conventions apply? Which operations are supported? What evidence exists for each step?
- Lean can check formal consequences rigorously. Given a suitable formal statement and foundations, does the proof type-check?
- Experiments and observations constrain physical truth. Neither a Phys replay nor a Lean proof alone establishes that a model describes Nature.
This is not a perfect wall between “input” and “output.” Lean can expose a bad formal statement, and Phys can test transformations and challenge incorrect outputs. But their strengths differ. A Lean proof may be completely valid while the theorem formalizes the wrong interpretation of a paper. A faithful Phys source map may document a claim accurately while an algebraic step remains unproved. We need both kinds of discipline.
A future integration could let Phys attach the source, assumptions, interpretation, regime, and provenance to a claim, then export a precisely scoped mathematical subproblem to Lean. The checked theorem and its dependency/axiom information could be linked back to the corresponding derivation step in Phys. That bridge is a proposal, not an existing integrated product. The useful principle is to preserve the context around a proof rather than treating a green checkmark as the end of scientific review.
Human judgment and autonomous agents both matter
Requiring a human to approve every algebraic transformation would waste the value of automation. Let agents do useful work on their own within explicit boundaries: enumerate candidate assumptions, search libraries, propose subgoals, try derivations, generate counterexamples, run unit tests, compare a hypothesis with a null model, and report which steps failed. They can iterate quickly and explore branches that a person might not have time to pursue.
But autonomy needs structure. Agent tasks should be bounded, reproducible, and reversible. The workflow should record the source and dependency versions, run tests in a controlled environment, distinguish generated candidates from accepted claims, and stop rather than inventing an unsupported rule or silently changing the specification.
Humans remain essential for choosing worthwhile questions, judging the intended meaning of a physical concept, reviewing source fidelity, deciding whether assumptions are reasonable, weighing empirical evidence, and taking responsibility for scientific conclusions. These judgments cannot be replaced by adding more retries to an agent loop.
The goal is not “human in every step” or “human out of every step.” It is human authority over meaning and acceptance, with machine autonomy for transparent exploration and checking wherever the task is well-defined.
What exists today—and what does not
Phys has moved beyond a slogan. The work includes a documented cross-project architecture, a theory-neutral mathematical library, physical-framework packages, source and derivation guidelines, and a workflow contract for two kinds of work: formalizing a derivation from a paper and solving a specified textbook or benchmark problem. The current paper-scale example includes a bounded Bohmian minisuperspace fixture based on a portion of the Dürr–Struyve Quantum Einstein Equations paper; it is not a formalization of the entire paper or proof of the theory's empirical truth.
Adversarial testing has also exposed an important failure mode: an AI solution can import a library without meaningfully using it, include dead or stubbed tests, invent a symbolic rule, or pass a test suite that never checks the intended physics. The workflow therefore requires actual API use to be exercised by tests, independent expected results where appropriate, and explicit reporting of gaps and limitations. “The tests pass” is evidence only for what the tests really test.
The boundaries matter too. Phys is currently focused on theoretical representation and supported symbolic operations—the work physicists often perform with pen and paper. Numerical solvers, Monte Carlo methods, a complete dimensional-semantics system, and autonomous scientific discovery are not delivered by the current infrastructure. The planned MCP setup and polished end-user demo are further work, not something this article claims is already deployed.
A practical first step: make every answer leave evidence
The public demonstration is designed around two reusable workflows:
Paper derivation: choose a bounded result from a physics paper, pin the source version, map the quantities and assumptions, audit the available capabilities, and create a conforming formalization package. Tests should distinguish what is represented from what is actually executed or replayed. Any unexpressible requirement stays a visible gap rather than a new, improvised schema field.
Textbook problem: identify the problem and its conventions, perform the capability audit, use Phys where it genuinely fits, and record exactly which APIs and tests exercise the claimed reuse. Any unsupported numerical computation stays local and is not attributed to Phys. The package reports the answer, reasoning, test outcomes, and limitations.
This gives people a way to see AI-assisted research as something other than a chat transcript. A student, researcher, or reviewer can ask: What is the source? What was assumed? What ran? What failed? What did the test establish? What remains a human judgment?
The project needs help from Go developers, physicists, mathematicians, formal-methods researchers, educators, and people who care about responsible open-source AI. Contributions can start small: reproduce an example, add an independent expected result, build a test that catches a plausible mistake, improve documentation, or review whether a formalized statement preserves the source's meaning. Academic groups can bring real paper fragments and expert review; industry partners can support testing, reproducible infrastructure, and integrations; sponsors can fund sustained maintenance and independent validation.
The bigger idea: a common ground for research
Today, a physicist may describe a model in a paper, a mathematician may formalize one of its theorems, a software engineer may implement a calculation, and an AI agent may propose a new hypothesis. Too often, these artifacts live in different languages and tools, with unclear links between the assumptions, the code, the proof, and the scientific claim.
Phys is an attempt to create common ground: a research artifact that people can read, agents can work with, and software can test. Go is the executable engineering layer for the current libraries and protocols. Lean and similar proof systems can provide stronger formal checking for suitable claims. Human reviewers preserve scientific meaning and judgment. Empirical work supplies the reality checks that mathematics alone cannot provide.
The promise is not that hallucinations disappear, or that a test suite will tell us the final truth about the universe. The promise is that unsupported claims become harder to hide, useful exploration becomes easier to reproduce, and AI can help more people participate in science without asking them to trust a confident answer blindly.
Phys is open source, and it needs collaborators. Explore the repositories, try the workflows, challenge the assumptions, and help us make research with AI more transparent, testable, and useful.
Explore the project
Project status note: Phys–Lean integration, automated hypothesis discovery, and the public MCP demo are directions for future work, not claims of currently completed functionality. The current scope and capabilities should always be checked against the live repositories, implementation, and tests.
Top comments (0)