Agentic and Neuro-Symbolic AI for Mathematical Research

Research-attempt provenance

Definitions and mathematical statement

Shared notation.

Standard number systems are $\mathbb N,\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$. Specialized notation and index ranges follow the cited source and the definitions below.

A symbolic deduction system specifies inference rules that can be checked exactly. A neural model supplies statistical pattern predictions; an agent architecture combines these with a procedure for selecting tasks, tools, and candidate deductions.

Record scope and qualifications.

The catalogue title is retained as metadata. Named certificates, contracts, bounds or frameworks in that title are not asserted as results of the original source extract. This is a system-design and benchmark direction. No definite mathematical correctness, novelty, or performance theorem is stated.

Source-record limitation: An autonomous research-agent architecture and benchmark performance are requested without a mathematical statement.

Statement recorded in the supplied source.

Build an agentic AI system that carries out the full workflow of a mathematician, from exploring examples and formulating conjectures to selecting proof strategies, and determine whether it can solve research-level benchmarks such as FATE-X autonomously. Identify an effective architecture that combines neural pattern recognition with rigorous symbolic deduction to produce novel, human-readable, formally checkable proofs. [S2]

Source status.

The supplied catalogue labels this source record open; that metadata was checked against the supplied snapshot on 2026-10-11. The label is preserved for provenance and is not an independent verification of present open status or mathematical correctness. The catalogue literature assessment is dated 2026-08-22.

Short English statement

Build autonomous mathematical-research systems combining neural prediction and checked deductions.

Sources

• S1 Ulam AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 30006439 (OWR-14299525-003). Catalogue curation and metadata: CC BY 4.0. The source extract is retained; definitions, English summaries and qualifications are editorial additions. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 MATRIX-MFO Tandem Workshop: Machine Learning and AI for Mathematics $2026$, Oberwolfach Reports, DOI 10.4171/owr/2025/43, pp. 2323--2350 https://doi.org/10.4171/owr/2025/43.
• S3 FATE benchmark https://arxiv.org/abs/2511.02872.
• Source-specific Oberwolfach Reports licences, including CC BY-SA 4.0 where applicable, are retained; see THIRD_PARTY_NOTICES.md.

Preparation and review.

The original source and UnsolvedMath contributors retain attribution for the source extract. Codex (GPT-6; exact serving revision not exposed) assisted with definitions, English summaries, scope notes and formatting. No new human mathematical authorship or independently verified solution is asserted. Permanent source ID 30006439 and code OWR-14299525-003 checked against the complete supplied registry and current repository. Distinct upstream records, including repeated questions and broad or damaged extracts, are retained for complete coverage of the source CS category. A repeated record is not a new independent conjecture. Complete mathematical-equivalence and current-literature review has not been performed. Preparation and final review follow contribution prompts C and D, with source gaps disclosed. Structural and rendering checks do not establish a new theorem or open status.

Literature and context check

The primary report, printed pp. 2335--2336, poses an agentic full-mathematical-workflow and research-benchmark agenda. No benchmark performance or general architecture result follows from the finite model below. It investigates a concrete fragment in which heuristic proposal, proof construction, counterexample production, and guaranteed completion can all be separated rigorously.

Research attempt: A complete bounded Horn research loop with explicit certificates

Let $U$ be a finite set of $N$ propositional atoms, $F\subseteq U$ initial facts, and a finite set of Horn rules $P\to a$ with $P\subseteq U$, $a\in U$. Empty premises are allowed. Form a closure by starting with $C=F$ and repeatedly adding the head of any rule whose premises are all in $C$. Each effective addition increases $|C|$, so there are at most $N$ additions. At termination every rule with all premises in $C$ has its head in $C$.

The final set is independent of the order and exactly characterizes entailment of atomic goals. Every model of the facts and rules contains each newly added atom, by induction over additions. Conversely, the truth assignment making exactly $C$ true satisfies the facts and every rule: if its premises are true they lie in $C$, and closure places the head in $C$. Thus a goal $a$ is entailed if and only if $a\in C$. If it is, recording the rule and previously recorded premises at the first insertion gives an acyclic readable proof. If it is not, the assignment $C$ is an explicit countermodel.

A queue implementation is linear in the input incidence size. For each rule store a counter of premises not yet true and, for each atom, a list of rules containing it. Insert facts once, decrement a counter when its previously false premise first becomes true, and enqueue the head when the counter reaches zero. Each atom is inserted at most once, every premise incidence is processed at most once, and every rule is activated at most once. Initialization includes all rules and atoms, so the bound is \[ O\left(N+\#\text{rules}+\sum_{P\to a}|P|\right). \] Duplicate premises are removed in the set representation. Empty-premise rules are activated at initialization.

Role and limit of a learned proposer.

An untrusted learned component may prioritize enabled rules or propose short derived lemmas, provided every insertion is verified against already accepted facts. Soundness remains the induction above. Completeness additionally requires the queue to process every enabled rule eventually; a heuristic that indefinitely revisits an unproductive rule need not find an existing derivation. A fallback queue provides this guarantee in the finite fragment.

For example, rules $p\to q$ and $q\to p$ with no facts do not prove either atom. A purported circular derivation citing each as the other's support is invalid; the closure is empty and its all-false assignment is a model. With fact $p$, the rule $p\to q$ gives a valid one-step proof of $q$. This example shows why merely assembling mutually supportive generated lemmas is not a proof certificate. The finite rule/atom universe makes termination possible here; a mathematical research system generating new definitions and conjectures need not remain in such a bounded closure.

Verification and adversarial audit

Both directions of entailment were proved, yielding an actual countermodel on failure rather than reporting a timeout. The proof record is acyclic because every premise was already inserted. Queue complexity includes empty rules, all atoms, and all premise incidences. Learned prioritization is permitted only with a fair complete fallback and verified insertions.

Audit corrections.

Did not equate heuristic termination or mutually supporting claims with proof; stated the finite-universe and fairness conditions needed for completeness.

External computation.

None; symbolic arguments and boundary checks only.

Scope and remaining gaps

The source's open-ended theorem discovery, natural-language interpretation, research-level FATE-X tasks, and optimal neural/symbolic architecture are not solved. This is a bounded formal fragment with a fully worked algorithm and a precise boundary to the general agenda.

Integration review.

Codex (GPT-6; exact serving revision not exposed) reviewed the written arguments and expanded layout and source-reference wrappers. Repository metadata and the production web renderer were checked using Python 3.13 and JavaScript with MathJax 3.2.2. This model-assisted review is not independent human proof verification; no PDF compilation or formal proof checking is asserted.

Completion Estimate

COMPLETION: 0% The calculations below the preserved source statement investigate a concrete route, but establish no substantiated new progress toward the entire original target. Known special cases and failed sufficient conditions are not credited as a solution.

References

The original source references and catalogue attribution are preserved in the Sources section above. The following URLs were actually consulted for this attempt; retention of an additional original reference does not claim fresh consultation of it.

• https://ems.press/content/serial-article-files/52253 (consulted 2026-10-11).

Model and contributor disclosure

Codex GPT-6 completed written-proof review of this attempt at its declared scope; this is model-assisted review, not independent human proof checking. OpenAI gpt-6-astra, requested reasoning configuration ultra, generated this research attempt on 2026-10-11. The exact serving revision is not exposed. Codex GPT-6 performed orchestration and repository-format review; its exact serving revision is also not exposed. The mathematical route, boundary checks and final adversarial self-audit followed contribution prompts A then B in docs/contribution_prompts.md, after reading CONTRIBUTING.md. Python 3.14.2 assembled the standalone documents; any mathematical computation is specified in Verification. No theorem prover was used. No human mathematical authorship, substantial human proof correction, or independent human proof checking is asserted. Model-assisted review, source retrieval, and structural checks do not establish correctness or novelty. Full private reasoning transcripts are unavailable as reproducibility artifacts; the complete arguments, inputs and outcomes actually used are stated here or in the companion batch audit.

Final status

Unresolved as a new research contribution. This is a concrete route investigation, not a claim of new complete resolution or a current-status certification. A known answer reproduced for context does not become a new contribution. The catalogue's source-status label is preserved; this attempt status does not assert that a source-labelled solved question is open.