A practical roadmap for logic research agents

1

Recommendation

Use one research loop, but keep generation, checking, and explanation separate.

Start hereStage 1

Semantics and countermodels

Make the logic, frame conditions, domains, consequence relation, and fixed definitions explicit. Try to break the conjecture before trying to prove it.

Add nextStage 2

Retrieval and tool orchestration

Connect theorem-level search, proof planning, model finders, provers, proof assistants, and a reproducible run ledger.

DelayStage 3

Open-ended proof and system discovery

Attempt new metatheorems, conjectures, axioms, or logical systems only after the system can audit statements and verify results independently.

The complete research loop

1Specify the questionLanguage, semantics, consequence, boundaries
2Retrieve prior workTheorems, definitions, counterexamples
3Attack the conjectureModels and assumption stress tests
4Plan the proofSubgoals and dependencies
5Use the right toolsProvers, solvers, model checkers
6Verify independentlyKernel, certificate, or separate checker
7Digest the resultKey lemmas, structure, explanation
8Record provenanceSources, versions, failures, cost

A run is complete only when it states the logic in use, the exact result, why it holds, where it fails, and how it relates to known work.

2

Why this is worth building now

The opportunity comes from the workflow around the model, not from one-shot proof generation.

Research-level mathematical work is becoming testable

Recent systems combine informal planning, theorem retrieval, formalisation, compiler feedback, and repeated attempts. Results vary by benchmark and review status, but the useful engineering pattern is now visible.

Logic has unusually precise feedback

SAT and SMT solvers, finite-model finders, proof assistants, and model checkers can reject many errors cheaply. This makes logic a good setting for agent workflows whose claims must be checked.

Semantic errors remain the main product risk

The same formula may behave differently under another frame class, domain policy, or consequence relation. A correct formal proof is not enough if the formal statement does not match the researcher's intended claim.

Design implication

The system should treat the semantic configuration as a contract. Changing that contract is a visible research decision, not an automatic repair.

3

Build order

Each stage has a clear purpose and an exit condition.

Stage	What to build	Main components	Exit condition	Likely research output
1 Build now	Semantic audit and countermodels Explicit specifications, finite Kripke search, assumption testing, reproducible records	SpecGuard Counterexample Lab Proof PR Guard	Distinguishes invalidity, semantic mismatch, encoding error, and tool timeout	Compliance benchmark, countermodel dataset, conjecture-repair methods
2 Add next	Knowledge and orchestration Theorem graph, proof DAG, tool adapters, checked translations	LogicAtlas LogicOS ProofDAG PolyLogic Bridge	Every retrieval resolves to a theorem, version, and assumptions; every tool conversion is traceable	Theorem graph, common tool protocol, cross-logic test suite
3 Open later	Proof and theory exploration Metatheory, conjectures, new definitions, proof digestion, library maintenance	MetaProver LogicFoundry ProofDigest LogicLib Maintainer	New results have certificates, attribution, failure boundaries, readable explanations, and human approval	Reusable metatheory, proof-pattern library, controlled exploration studies

The three best first products

1
Modal and epistemic semantic workbench
Combine semantic auditing, finite countermodel search, and checked translations. This is the strongest research direction because it has a clear identity within logic and produces useful evaluation data.
2
Proof PR Guard
Compare paper statements, informal arguments, formal code, and citations. This is the fastest component to place in a real research team's workflow.
3
LogicAtlas
Build theorem-level links between systems, definitions, frame conditions, metatheorems, counterexamples, formal libraries, and original sources.

4

Component catalogue

Twelve specialist roles. Scores are product judgements, not literature rankings.

Component	Job	Typical output	Need	Feasibility
Specification and intake
SpecGuardSemantic auditor	Compare prose, formulae, and prover statements; check domains, consequence, frames, designation, types, and base logic.	Semantic diff, back-translation, risk report	10	8
Counterexample LabModel and assumption testing	Enumerate finite structures and Kripke frames, call model finders, weaken assumptions, and seek minimal countermodels.	Countermodel, failure world, sensitivity matrix	10	9
Spec-to-ModelRequirements formalisation	Translate system requirements into temporal, epistemic, deontic, or program specifications and run model checking.	Executable specification, conflict analysis, witness trace	9	8
Planning, solving, and translation
LogicOSTool orchestration	Choose tools for subgoals, manage sound conversions, recover certificates, and classify failures.	Tool plan, conversion log, certificate	9.5	6
ProofDAGProof architecture	Turn a human strategy into dependent subgoals and route work to retrieval, model, proving, and review components.	Proof blueprint, task DAG, decision points	9	8
MetaProverLogic metatheory	Support soundness, completeness, cut elimination, finite-model properties, interpolation, correspondence, and complexity.	Metaproof plan, formal certificate, failure witness	8.5	6
PolyLogic BridgeTranslations and embeddings	Check preservation, reflection, frame restrictions, complexity changes, and imported principles across logics.	Translation, preservation proof, scope conditions	8.5	6
LogicFoundryControlled exploration	Propose axioms, rules, definitions, or semantic conditions and test novelty, non-triviality, consistency, and equivalence.	Candidate system, representative models, exploration log	7.5	5
Review, knowledge, and maintenance
LogicAtlasTheorem knowledge graph	Connect systems, axioms, semantics, metaproperties, counterexamples, dependencies, formal libraries, and sources.	Theorem-level retrieval, strength relations, attribution	9.5	7
Proof PR GuardIndependent proof review	Check circularity, undeclared lemmas, hidden axioms, definition drift, citation mismatch, and formal fidelity.	Review report, proof-mutation tests, blocking issues	9	8
ProofDigestProof explanation	Compress machine proofs, identify decisive lemmas and shared structure, and separate ideas from routine technique.	Concept map, proof patterns, layered explanation	8.5	8
LogicLib MaintainerFormal library work	Resolve duplicate definitions, build basic APIs, trim dependencies, manage namespaces and migrations, and bridge libraries.	Library refactor, compatibility layer, provenance record	8	9

5

Shared infrastructure

These requirements apply no matter which component is built first.

1

ProofLedger

Record sources, theorem numbers, paper versions, model and tool versions, prompts, human edits, failed paths, computational budget, and final certificates.

2

Explicit semantic configuration

“S4” or “classical first-order logic” is not enough. Frames, domains, consequence, equality, designation, and metalogic must be machine-readable.

3

Independent verification

The generator cannot be the only reviewer. Use a symbolic tool, proof kernel, or genuinely separate verification path for every critical claim.

4

Failure memory

Keep failed subgoals, countermodels, timeouts, broken formalisations, and abandoned routes. Failure records are useful research assets.

5

Human decision points

Changes to definitions, research goals, base logic, main proof strategy, and publication value remain decisions for the researcher.

6

Suggested first prototype

A finite-model workbench for propositional modal and epistemic logic.

Input contract

Logic: S4
Consequence: local
Frames: reflexive, transitive
Domains: constant
Equality: rigid identity
Premises: …
Conjecture: …
Locked: definitions, base logic

Required output

Valid, invalid, or currently unresolved
A minimal countermodel or machine-checked proof
An assumption-sensitivity matrix
A comparison across nearby logics such as K, T, S4, and S5
A plain-language explanation
The closest known theorem with a precise source
A complete, reproducible run record

Version 0.1	Extend next	Evaluation
K, D, T, B, S4, S5 Propositional modal logic Finite Kripke frames Local and global consequence Minimal countermodels	First-order modal logic Constant, varying, cumulative domains Multi-agent epistemic logic Dynamic epistemic logic Hybrid logic and model checking	Semantic-compliance rate Countermodel correctness and minimality Certificate acceptance rate Attribution and reproducibility coverage Accurate human restatement

7

What not to build first

These can make useful demonstrations, but they do not address the central reliability problem.

A PDF assistant that only chats about logic papers
A tactic autocomplete that only sees the current Lean state
A conjecture generator without literature and countermodel filters
A formaliser that never checks fidelity to the original statement
An autonomous research agent without certificates, sources, or failure records
A system that writes a full paper and declares its own novelty

Recommended order: semantic audit and countermodels → theorem graph and tool orchestration → proof generation and open exploration.

8

References and further reading

This guide is a research and product judgement, not a consensus ranking. Preprint claims remain subject to further review.

Institutional reportGemini Deep Think at IMO 2025Google DeepMind
PreprintAutomated Conjecture Resolution with Formal VerificationRethlas–Archon
Preprint130k Lines of Formal Topology in Two WeeksAutoformalisation
Institutional reportAccelerating scientific breakthroughs with an AI co-scientistGoogle Research
PreprintLogicSkills: A Structured Benchmark for Formal ReasoningSemantic compliance and countermodels
PreprintMathematical methods and human thought in the age of AITranslation, verification, and human control
RoadmapFrom Solvers to ResearchFormal mathematics at the research frontier
PreprintFormalizing a Many-Sorted Hybrid Polyadic Modal Logic in LeanReusable modal metatheory
PreprintMany Logics, One MethodologyLogical pluralism in formalised reasoning
InterviewKevin Buzzard on LLMs and formalisationNebius Science
PreprintMathematicians in the Age of AIHuman agency and auditable mathematics