mw / Notes on the laboratory ↗

Notes on the laboratory / Edition 01

Evidence before interpretation.

Mathematical Worlds asks you to do an experiment, observe a structure, and confront a philosophical question. Each mathematical result carries its method and source.

Four kinds of provenance

✓ Computed

Exact arithmetic, closed-form algorithms, symbolic certificates or exhaustive finite checks. This is programmatic verification, not a proof-assistant guarantee.

◇ Curated

A definition or mathematical theorem transcribed with a reference and explicit assumptions. The software can apply the relation without independently proving it.

✓ Formal proof

Reserved for a checked proof artifact with its system, version, declaration and axioms. No result in this edition uses this label.

Interpretation / Discussion

Philosophical lenses and questions. Curated prompts are always available. Optional AI questions are clearly labelled and cannot write to the mathematical record.

The computation has a boundary.

The input grammar accepts bounded integers, fractions, square roots of nonnegative integers and real cube roots of integers. It does not execute arbitrary expressions. Six stored algebraic certificates are generated and checked with SymPy. Their JSON is included with the application; no Python service is needed during a visit.

A displayed decimal or graph is approximate. It is never the evidence for algebraicity, irreducibility or transcendence. The constructibility test only concludes “yes” when an explicit construction is known. A power-of-two degree alone is not enough.

The framework has a name.

Choice equivalences are stated over classical ZF, including Infinity. Independence is qualified by consistency. Withholding an axiom and adding its negation are separate actions. Unknown combinations remain “Not modelled.” The intuitionistic controls expose a propositional-logic lens, not a complete implementation of intuitionistic set theory.

One group, several senses of sameness.

The Identity Lab accepts a bounded mathematical notation grammar. Finite groups are checked through exact operation tables and verified isomorphism witnesses. Classical matrix groups use sourced theorems and invariants: equal dimension alone proves no isomorphism. Abstract groups, Lie groups and real Lie algebras are separate comparisons. The SU(2) double-cover diagram illustrates a theorem; sampled matrices do not prove it. Unmodelled comparisons remain undetermined.

A place for AI, without mathematical authority.

The optional discussion service receives a fresh server-side evidence record for a selected object. Its output contains only philosophical questions. It cannot modify properties, certificates, dependencies or sources. Generated questions are interpretations and may still frame an issue poorly; their wording is not verified. This edition works completely without an AI key.

The schema reserves adapters for symbolic, curated and formal verification. A future Lean adapter can attach checked declarations and axiom reports; SageMath can provide larger algebraic calculations through the same evidence contract.

References in this edition

Begin an experiment →Return to the laboratory →