# Research program

## Central question

Can a hypothesis-generating machine produce useful formal results under an
explicit specification, with acceptance determined by reproducible checking?
The knowledge base supplies a common language for problems, claims, evidence,
checker scope, and explanation. It covers 22 areas with 66 worked records.

## What is implemented

The corpus supports complete finite search, reachable-state exploration,
syntax-directed typing, exact reduction replay, rational Markov propagation,
interval containment, GF(2) elimination/kernel enumeration, and other domain
checks. It contains satisfiable and unsatisfiable formulas, positive and negative
equivalence results, sound interval summaries, feasible optimal witnesses,
winning strategies, and unsafe protocol traces. The browser offers twelve
interactive computation views. This is a reference collection, with no
model-performance evaluation attached.

## Verification depth

Expand each family along four axes: richer formal objects, larger domains,
stronger certificates, and independently reviewed exposition. Prefer certificates
whose checking is cheaper and easier to inspect than candidate search. Examples
include flow/cut equality, assignment primal/dual equality, checked UNSAT logs,
DFA equivalence partitions, and row-operation/nullspace-basis certificates.
Keep finite coverage distinct from unrestricted proofs.

For semantics and types, add typed environments, effect models, stuck states,
recursive definitions, and derivation certificates. For systems, add message
queues, explicit loss/duplication, fairness, and temporal properties. For databases,
add bag multiplicity and NULL semantics. For probability, add exact hitting-time
and reachability equations before moving to nondeterministic models.

## Hypothesis-generation study

Begin with Boolean circuit synthesis under a fixed basis and budget. Generate
candidate circuits, check every truth table independently, and establish
minimality through complete smaller-circuit search where feasible. Report an
upper bound and objective gap when minimality is unresolved. Record all attempts,
model/build, prompt, seed, sampling parameters, time, and resource use.

Define the target function split and baselines before running the study. Compare
with enumeration and simple synthesis heuristics. Keep public reference examples
separate from held-out target functions. Judge verified validity, objective
quality, accepted result rate, and computational cost separately.

## Review, preservation, and rights

Review specifications, checker implementations, enumeration completeness,
certificate coverage, source references, and language explaining scope. Store
reviewer identity and decision before assigning independent-review status.
Select explicit licenses for text/data and code before presenting the corpus as
open-licensed. Preserve every distributed source version and document corrections.

## Research milestones

1. Independently review the 22 input models and checker families.
2. Add scalable certificates for three optimization or equivalence families.
3. Establish a registered model-generation protocol and lineage-based splits.
4. Run and publish the first complete attempt-log evaluation with baselines.
5. Introduce proof-assistant artifacts where they provide useful stronger claims.