Research / 01 / Formal systems
Formal
Computer
Science.
A knowledge base for problems with explicit rules, inspectable evidence, and answers a machine can check.
Specify the problem. Generate a hypothesis. Verify the result.
Rules before results.
These are formal questions, rather than observations about nature. Once the specification is fixed, its truth conditions stay fixed. A problem can have many valid solutions; verification must match the exact claim.
Make the question exact.
Declare inputs, semantics, constraints, and the property or cost being measured.
Produce a candidate.
An algorithm, model, derivation, circuit, schedule, or transformation is a hypothesis until checked.
Replay the evidence.
Check the witness or certificate. State bounds, assumptions, checker identity, and failure conditions.
Keep the claim inspectable.
Release readable exposition with source, provenance, verification scope, and a separate review status.
The pilot corpus.
Eleven small, reproducible examples establish the format. Every entry passes its declared mechanical check and awaits independent review. This is infrastructure for future research; no model performance or novel discovery is claimed.
11 of 11 entries · mechanically checked / awaiting review
No matching entries. Try another term or reset the filters.
Publishing standard.
A readable explanation and a checker pass answer different questions. We preserve both, including what they leave unresolved.
The entry is the unit of knowledge.
Each entry combines an explicit problem, formal payload, candidate result, evidence, replay instructions, explanation, limitations, references, and provenance. JSON supports machines; Markdown supports readers.
Finite validation is labeled with its bounds. Optimality requires evidence that better solutions are impossible in the stated model. Unknown and timeout remain unresolved.
Download the full publishing guidelines ↗Checking and review stay separate.
- Draft: formulate the problem and candidate.
- Mechanically checked: the named checker accepts the exact artifacts.
- Independently reviewed: assess semantics, evidence, trust, and exposition.
- Validated release: freeze reviewed records with source, hashes, rights, and a changelog.
Current state: experimental pilot. All 11 entries await independent review. The checker uses Python and custom finite procedures; no proof-assistant validation is claimed.
Read it. Replay it.
The source bundle includes every pilot record, Markdown entry, checker, rejection check, schema, verification report, and project guide. Python 3.9+; no extra packages.
After extracting the bundle, run python3 tools/verify.py and python3 tools/check_checker.py. The report identifies the exact corpus and checker hashes. This pilot is source-available for inspection and reproduction; an open reuse license has not yet been selected.
The publishing approach is informed by Algebrica’s coherent explanations, downloadable source, semantic structure, and transparent editorial process. These pilot records are original Kenton Labs examples; no Algebrica content is included.