| name | gaia-formalize-fine |
| description | Use when formalising a knowledge source (scientific paper, textbook chapter,
technical report) into a Gaia knowledge package and you want the thorough,
audit-grade treatment. Walks a six-pass pipeline — extract → connect → check
completeness → refine strategy types → verify structural integrity → polish
for standalone readability — with a compile + check loop after every pass and
a prior-assignment + inference tail. Emits the package source, `priors.py`,
and `ANALYSIS.md`. This is the **Paper → package** entry point when depth
matters: the slow, exhaustive sibling of `gaia-formalize-coarse` (which is a
quick four-phase single-pass for one paper). Reach for `gaia-formalize-fine`
when the source is load-bearing, multi-section, or destined for publication;
reach for `gaia-formalize-coarse` for a fast first cut of a single paper.
|
Knowledge-package formalization
Drive an agent through formalising a source (scientific paper, textbook chapter, technical report) into a Gaia knowledge package. The output is DSL source under src/<pkg>/ — claim, derive, infer, observe, compute, equal, contradict, exclusive, decompose, note, question, compose statements authored either via the gaia author <verb> CLI or by hand — plus priors.py for leaf-claim priors, plus a critical-analysis ANALYSIS.md deliverable. Every CLI verb the skill calls is on gaia today; the skill is the methodology that surrounds them.
Overview
Formalization is a six-pass process. Each pass builds on the previous one. Do not skip passes or combine them.
Key principle: formalization is incremental. After completing each pass, write code, compile, and check. Do not wait until all passes are done before writing code. Feedback from gaia build compile and gaia build check is critical input for the next pass.
Pass 1: Extract → write DSL code
↓ gaia build compile + gaia build check
Pass 2: Connect → wire premises to conclusions with derive / infer / observe / compute / decompose; add equal / contradict / exclusive
↓ gaia build compile + gaia build check
Pass 3: Check completeness → @labels audit, missing reasoning, isolated nodes
↓ gaia build compile + gaia build check
Pass 4: Refine strategy types → tighten infer → derive / compute / observe / compose
↓ gaia build compile + gaia build check
Pass 5: Structural integrity → operator semantics, double-counting elimination, hidden-evidence-in-reason, shared-dependency extraction
↓ gaia build compile + gaia build check
Pass 6: Polish → self-containedness, figures, formatting
↓ gaia build compile + gaia build check
gaia build check --hole → write priors.py
↓
gaia run infer . → .gaia/beliefs.json
↓ Interpret BP results (see ../_shared/bp-interpretation.md)
↓ ┐
│ structural issues → back to Pass 1-5
│ prior issues → revise priors.py
└ otherwise → ANALYSIS.md → gaia run render --target github
| Pass | Focus | Core question |
|---|
| 1 | Content extraction | Are claims and notes extracted? Atomic? |
| 2 | Reasoning connections | Are derivations, inferences, observations, computes, and structural relations modelled? |
| 3 | Content completeness | Any missing premises, orphans, or @label errors? |
| 4 | Strategy precision | Is each author verb the right one (derive vs infer vs compute vs observe vs compose)? |
| 5 | Structural integrity | Is evidence independent? Are contradict / exclusive semantics correct? |
| 6 | Standalone readability | Can a reviewer understand everything without the source? |
Scope
Formalize the complete source — not just the main result. A partial formalization leaves reasoning gaps: premises without support, alternatives without comparison, intermediate steps without justification. If the source is too large (a full textbook, say), formalize one chapter at a time, each as a separate Gaia package.
CLI invocations referenced by this skill
The methodology below leans on this fixed set of CLI calls. Drill into gaia <group> <verb> --help when you need exact flags.
gaia pkg scaffold --target <name>-gaia --name <name>-gaia --namespace <ns> [--with-uuid] [--description "..."] — fresh package skeleton (pyproject.toml, src/<import_name>/__init__.py, .gaia/.gitkeep). The import name is derived from --name (strip the trailing -gaia, hyphens → underscores); the CLI emits a JSON envelope. Does not create artifacts/ or references.json — make those manually.gaia pkg add-module --name <module> --target <name>-gaia [--imports <verbs>] — scaffold a sibling module under src/<import_name>/ (e.g. motivation, s2_xxx, priors). --imports pre-seeds DSL-verb imports (e.g. --imports register_prior).gaia build compile <pkg> — lower DSL → IR (.gaia/ir.json). Run after every pass.gaia build check <pkg> — structural validation + role classification (independent / derived / structural / background / scaffolded / orphaned). Use between passes:
gaia build check <pkg> --brief — per-module overview with strategy summaries.gaia build check <pkg> --show <module-or-label> — expand a single module / claim / warrant tree.gaia build check <pkg> --hole — list independent claims missing priors (with content + QID).gaia build check <pkg> --gate — publish-readiness gate (CI-friendly, non-zero on failure).
gaia author <verb> — append a DSL statement and re-check. The verbs you will use most:
gaia author claim — declare a claim(...) knowledge node (use when first surfacing a proposition).gaia author note — declare a note(...) background statement (use for mathematical definitions, formal setups, fundamental principles).gaia author question — declare a question(...) research question.gaia author derive --conclusion ... --given ... — author a directed implication: premises rigidly support the conclusion. Carry --rationale for the natural-language justification; relation quality is reviewed through the rationale and gate workflow, not through a prior on the derived conclusion or helper.gaia author infer --evidence ... --hypothesis ... --p-e-given-h ... — author a Bayesian update on new evidence; the --p-e-given-h likelihood is required, --p-e-given-not-h defaults to 0.5.gaia author observe --conclusion ... [--value ... --error ...] — author a measurement event tied to a Claim, Variable, or Distribution.gaia author compute --conclusion-type ... --fn ... --given ... — author a deterministic-computation step (a named callable produces the result Claim).gaia author decompose --whole ... --parts ... --formula-template and|or|atom — split a composite claim into atomic parts.gaia author equal --a ... --b ... — equate two claims (logical equivalence).gaia author contradict --a ... --b ... — assert NOT (A AND B): both cannot be true, but both can be false.gaia author exclusive --a ... --b ... — assert A XOR B: exactly one must be true (exhaustive + mutually exclusive).gaia author compose --from-file pattern.py — register a @compose-decorated reusable reasoning pattern.gaia author register-prior --claim ... --value ... --justification ... [--file priors.py] — write a register_prior(...) statement; auto-injects the import if the target file is a sibling.
gaia run infer <pkg> — run BP, emit .gaia/beliefs.json. Pass --depth N (>0) to merge dependency packages' factor graphs for joint cross-package inference.gaia run render <pkg> --target github — generate .github-output/ README + narrative outline (handoff to ../gaia-publish/SKILL.md).gaia run render <pkg> --target docs — per-module Mermaid graphs in docs/detailed-reasoning.md.gaia run render <pkg> --target obsidian — gaia-wiki/ skeleton (handoff to ../gaia-obsidian-wiki/SKILL.md).
Author verbs accept either an existing identifier (--conclusion my_claim) or auto-author the conclusion in-line (--conclusion-content "..."). Every authored statement supports --dsl-binding-name (Python LHS) and --label (engine label= kwarg) — assign both when the statement needs to appear in gaia build check --brief output and be referenceable by downstream verbs.
Pass 0 — Prepare artifacts
Copy the source materials into the package's artifacts/ directory, and create a references.json for bibliographic citations.
my-package-gaia/
├── artifacts/
│ ├── paper.pdf
│ ├── paper.md
│ └── figures/...
├── references.json
├── src/
│ └── my_package/
│ ├── __init__.py
│ ├── motivation.py
│ └── ...
└── pyproject.toml
gaia pkg scaffold creates pyproject.toml, src/<import_name>/__init__.py, and
.gaia/.gitkeep; per-section modules (motivation.py, s2_xxx.py, ...) are added
with gaia pkg add-module. Neither command creates artifacts/ or
references.json — make those manually.
references.json
Bibliographic citations in CSL-JSON format (dict-by-key), shared across the entire package. Start with a minimal skeleton; fill incrementally as citations are needed during Passes 1-4:
{
"Dias2020": {
"type": "article-journal",
"title": "Room-temperature superconductivity in a carbonaceous sulfur hydride"
}
}
Keys must follow Pandoc citation-key grammar (letters, digits, _, -, ., :, /). Each entry requires type (CSL 1.0.2) and title at minimum. Add new entries as you hit citations; do not enumerate everything upfront. Complete metadata (authors, DOI, volume, pages) is filled in during Pass 6.
references.json is optional — without it, [@...] citations are not available.
Both PDF and markdown formats are supported for artifacts. Throughout formalization, refer back to the originals in artifacts/ to keep numbers, formulas, and reasoning steps consistent with the source.
Progressive Workflow
After Pass 0, create a session todo list with the seven items below. Mark only
Pass 1 in progress. Do not load a later pass's reference file until the current
pass is complete and its compile + check inner loop passes — each pass
builds on the working state the earlier passes produced.
- Pass 1 — Extract knowledge nodes — load
references/pass-1-extract.md.
- Pass 2 — Connect: write reasoning relations — load
references/pass-2-connect.md.
- Pass 3 — Check completeness — load
references/pass-3-completeness.md.
- Pass 4 — Refine strategy types — load
references/pass-4-strategy-types.md.
- Pass 5 — Verify structural integrity — load
references/pass-5-structural-integrity.md.
- Pass 6 — Polish for standalone readability — load
references/pass-6-polish.md.
- Prior assignment, inference, ANALYSIS.md, render — load
references/priors-analysis-render.md.
Run the compile + check inner loop (below) after every pass. The six-pass
split is cumulative scaffolding — the emitted package must reflect all passes
as one coherent body of work, not six independent passes.
Inner loop: compile + check after every pass
After completing each pass, write code, compile, and check.
gaia build compile <pkg>
gaia build check <pkg>
gaia build check <pkg> --hole
gaia build check <pkg> --brief
gaia build check <pkg> --show s6_xxx
gaia build check <pkg> --show label
What to check in default output:
- Each independent premise shows
prior=X if set, or ⚠ no prior if missing.
- The summary shows "Holes (no prior set): N" when any holes remain.
What to check in --hole output:
- Every hole claim has its content and QID listed — use this to write
priors.py entries.
- Every covered claim shows its prior value and justification — verify these are reasonable.
What to check in --brief output:
- Every relation should show named labels (not
_anon_xxx). If a relation's conclusion shows _anon_xxx, the Python LHS was not set — re-author with --dsl-binding-name.
- Claims should show their role (independent / derived / structural / background / scaffolded / orphaned) and prior if set.
- Use
--show <module> to inspect full claim content and warrant trees for review readiness.
Common mistakes
| Mistake | Consequence | Fix |
|---|
| Theoretical prediction and experimental result mixed in one claim | Cannot model the verification relationship with infer | Separate into two claims + infer(evidence=obs, hypothesis=pred) |
infer without a meaningful alternative or with --p-e-given-not-h left at 0.5 when the source argued otherwise | Bayesian update misses the competing-explanation force | Set --p-e-given-not-h from the source, or chain infer against each alternative hypothesis |
infer alternative's prior reflects "computational correctness" instead of "explanatory power" | π(Alt) too high, weakens evidence's pull toward H | π(Alt) answers "Can Alt independently explain Obs?", not "Is Alt's calculation correct?" (see ../gaia-review/SKILL.md) |
| Rationale written too briefly (one sentence) | Reasoning process is untraceable | Summarise derivation steps in detail, reference with @label |
4+ premise flat derive | Severe BP multiplicative effect | Use compose to decompose into sub-steps with 3 or fewer premises |
| Content not self-contained (symbols / abbreviations unexplained) | Reviewer cannot judge independently | Each claim must independently explain all symbols and abbreviations |
Marking a questionable proposition as note | That proposition cannot be updated via BP | When in doubt, mark as claim; only mathematical definitions are notes |
Marking a condition-dependent theoretical framework as note | Framework does not participate in BP | Condition-dependent conclusions should be claims |
Using derive for a Bayesian update | Loses the explicit P(E|H) / P(E|~H) the source supplied | Use infer with --p-e-given-h and --p-e-given-not-h |
Using infer for a step-by-step deterministic derivation | Forces a Bayesian update where rigid implication is the source's framing | Use derive with a detailed rationale; do not add a prior to the derived conclusion or helper |
Using derive for a numerical computation whose function is in code | Loses the deterministic-mapping framing | Use compute --fn ... with the named callable |
Anonymous relation (no --dsl-binding-name) | Relation invisible in gaia build check --brief, cannot be reviewed | Assign via --dsl-binding-name <name> --label <name> |
_-prefixed claim or relation | Node invisible in CLI output, gets no label | Use public names (no _ prefix); only __ is reserved for compiler |
| Missing prior for orphaned claim | gaia run infer errors | All claims (including orphaned) need priors |
| Missing implicit premises in reasoning | Knowledge graph is incomplete | Use gaia build check + manual review in Pass 3 |
| Not verifying numerical values | Data errors | Cross-check every value against the source |
| Same claim in multiple paths to same conclusion | Evidence double-counted, inflated belief | Ensure each leaf enters a conclusion through exactly one path (Pass 5) |
| Repeated observations with unmodelled shared dependency | Overcounted evidence | Extract shared dependencies as explicit claims (Pass 5) |
Wrong contradict (claims can both be true) | BP forced to suppress one side incorrectly | Verify structural-verb semantics in Pass 5 |
| Setting prior on derived claim | Double-counts evidence | Do not set priors for derived claims; inference engine defaults to 0.5 |
| Observation claim missing prior (classified as derived because it has incoming supports) | Observation's empirical grounding lost; belief depends entirely on theory relations instead of being anchored by data | Add observation to priors.py with high prior (0.9+), or use observe to tie it directly to a measurement value |
Reference Files
Passes (this skill)
Shared formalization methodology (../_shared/)
Shared with gaia-formalize-coarse; loaded by the passes that need them:
../_shared/formalize-extract-conclusions.md — what counts as a conclusion, fidelity, self-contained bodies, figures as prose, refs whitelist, citation form (Pass 1).../_shared/formalize-atomicity.md — one claim = one citable question, under-splitting traps, the two tests (Pass 1).../_shared/formalize-reasoning-chains.md — logic graph, topological order, reasoning-trace reconstruction, step rules (Pass 2).../_shared/formalize-independence.md — no-double-counting check, the four patterns, shared-factor extraction (Pass 5).../_shared/bp-interpretation.md — interpreting .gaia/beliefs.json (prior-assignment tail).
Sibling skills
