Neural-symbolic theologian

The prover follows the design of HyperTree Proof Search (HTPS): it splits a goal into smaller subgoals and proves them in turn.

The automated provers are Rocq's standard automation (firstorder, tauto, congruence, assumption) and, from round 4, CoqHammer, which sends a goal to the external provers Vampire and E and rebuilds any proof they find as Rocq tactics (sauto, sfirstorder, fcrush). The model's role is to divide the goals that the provers cannot prove by themselves.

The benchmark is the twenty steps of two classical arguments of Islamic theology for a first, uncaused cause — each concluding that something exists whose existence is from its own nature, received from nothing else.

Each step below is one of these twenty claims, written in Rocq from a small declared vocabulary and a few approved premises — nothing about God, time, or space is assumed. The prover is asked only to derive each step from the ones before it; the replay shows how.

This diagram replays the prover's recorded search on each test task. Each rectangle is a goal, exactly as Rocq displayed it; each rounded label is a step that was tried on that goal, coloured by who proposed it, and it links to the subgoals it left. Press Play to watch the search unfold step by step, or select any goal or step to read it in full.

The proofs of dalīl al-kalima and dalīl al-imkān are the test. They were never used as training data, prompts, or examples. At test time the model sees only the goal that Rocq displays: the vocabulary, the definitions, the postulates stated in the theorem, and the statement to be proved. The eight test tasks are listed, without proofs, in heldout_tasks.v.

The code is published below. The trained model weights and the CoqGym-derived training data are not, because CoqGym bundles third-party projects under their own licenses.

Each column is one way of searching for the proof. Symbolic only uses a fixed, hand-written list of steps instead of a model. The round-1 and round-3 columns use the trained model with Rocq's standard automation. CoqHammer alone is given each task directly, with no model. The last column is the current prover: the round-5 model divides the goals and CoqHammer, with the standard automation, proves the leaves. Each column is a single run.

Reading the table. The current prover proves six of the eight tasks in a single run. One of the six, the conclusion of dalīl al-imkān by the shorter route, is proved by no other column; CoqHammer alone does not prove it, either directly or after unfolding the definitions and taking the classical step. The other five are also proved by the hand-written list and by CoqHammer alone, so on those the model has not yet proved anything the existing tools could not. The higher-order prover Leo-III also proves the dalīl al-imkān conclusion directly; see the dalīl al-imkān report.

Budgets. Rounds 3 and 5: 256 to 512 expansions and 15 minutes per task; the other model columns: 64 expansions and 3 minutes. The hand-written list, given classical case splits and a larger budget (1,024 expansions, 10 minutes), still proves the same five.

Why two remain unproved. Premises 1 and 3 of dalīl al-kalima need reasoning over chains of causes of any length. That reasoning works only if one first states and proves a more general claim about every chain, and then applies it. The round-5 model now proposes statements about chains and generalizes its hypotheses before induction, but it has not yet proposed the general claim these premises need. Training aimed at this gap is under way. These results are very preliminary.

The first test above covered eight of the twenty steps of the two arguments. In a second test, the round-6 model attempted all twenty. It proved ten. The four new steps it proved are the four that CoqHammer also proves without a model; it did not prove the route of dalīl al-imkān through the aggregate (steps 6 to 12), or premises 1 and 3 of dalīl al-kalima. Its searches on all twenty steps can be replayed in Watch it search.

Each proof below was found by the prover and then compiled from scratch. Steps are written in Rocq's tactic language; braces enclose the proof of each subgoal. Proofs that use CoqHammer's tactics (sauto, sfirstorder, fcrush) need the CoqHammer tactics library, which the runner on this page does not have; their Rocq check output is linked.

In an earlier run on three tasks, the round-4 model proved the same conclusion by a different division: two cases.

Before CoqHammer was added, the round-3 model proved five of the eight tasks with Rocq's standard automation. In two of them it made the key step. These proofs were re-checked in Rocq 9.3.0.

What “pretrained, with no further training” means. A language model is first trained by its developer on a large body of text and code, and usually refined by the developer before release. A model in that state is called pretrained: it has a general command of language, mathematics and programming, but has not been trained for any particular task. The small model of version 1 was pretrained by its developer and then trained further by us, on proofs, for this task. Claude (model claude-sonnet-5-5, by Anthropic) was used exactly as released: we did not train it in any way, and it learned nothing from one attempt to the next. Neither model was ever given our proofs of the two arguments.

How it was run. Each call to Claude was isolated: no tools, no files, no internet, no memory of earlier calls. It was shown only the vocabulary, the declared starting points, any lemmas it had already proved for the current step, and the statement to prove. For each goal the automated provers were tried first. If they failed, Claude could propose complete proofs, or divide the goal into two to four subgoals, each then treated the same way. Rocq checked every proposal, and a division counted only when every subgoal was proved. The finished proof was compiled from scratch; the only logical assumption allowed was excluded middle.

Result. All twenty steps were proved in the first run, and again in a second run. The automated provers proved six steps without Claude. Of the other fourteen, Claude wrote the complete proof of nine in run 1 and divided five into lemmas; in run 2, ten and four.

Run 3: Claude states subgoals only. Because Claude wrote most proofs itself, a third run tested the design strictly: Claude could only state subgoals, never write a proof step, and every step of every proof had to be found by the automated provers (Rocq’s automation, a fixed tactic that applies induction to a chain and then calls the automation, and CoqHammer). It proved 16 of the 20 steps. Nine needed no division. The other seven, including premise 3 of dalīl al-kalima and steps 6–10 and 12 of dalīl al-imkān, were proved only after Claude divided them, sometimes over several levels; of the 111 lemmas in these proofs, Rocq’s automation proved 64 and CoqHammer 47. Four steps were not proved. For one of them, the conclusion without the “if”, Claude’s three subgoals are each true and together imply the goal, but the provers did not find the combination.

The same diagram for Claude, built from its three recorded runs on all twenty steps. In run 3, Claude’s only steps are divisions into subgoals; every proof step is by Rocq’s automation or CoqHammer. Select a step and a run; every rectangle is a goal, and every rounded label is a step that was tried on it: Rocq’s automation, a complete proof written by Claude, or a division of the goal into subgoals proposed by Claude. Select a division to read the subgoals Claude proposed.

Two divisions worth reading. For premise 3 of dalīl al-kalima (run 1), Claude first stated and proved, by induction, the general claim the small model never found: whatever depends on another through a chain of any length has its existence through it; from it, no chain returns to its start (pr003_no_circle.v). For the conclusion of dalīl al-imkān by the aggregate route (run 1), it divided the goal into seven lemmas, among them that no circle of existence-giving is possible and that, if no Necessary Existent existed, some aggregate would be given existence by one of its own members (imkan_s12_necessary_exists.v).

Limits. These are three runs, and Claude’s output varies from run to run. Every prompt was checked automatically against the 420 proof lines of our published Rocq files, and none appeared; but the data on which Claude was trained by its developer cannot be inspected, and our proofs were published in September 2026. A run was interrupted once by a fault in our test harness (a Rocq check exceeded its time limit); the two steps affected were run again, and the interrupted log is kept.

Files. Every prompt, every response and every Rocq check: run 1, run 2, run 3. Code: pilot.py (the search), pilot20.py (all twenty steps), heldout20.py (the twenty statements), verify20.py (the independent check), pilot_decomp.py (subgoals only).

The generated test problems are first-order problems that the automation cannot solve directly. They were never used in training.

Against the hand-written list, the round-1 model with the list proves 12 problems the list alone does not, and misses 1 that the list proves (sign test p = 0.003). Every configuration, with its limits, is listed in summary.csv.

• heldout_tasks.v: the first eight test steps, and heldout20_tasks.v: all twenty (statements only).
• Proofs found by the round-5 model with CoqHammer, with Rocq check output: imkan_b_necessary_exists.v, step3_possible_needs_cause.v, pr011_something_caused.v, kalima_first_cause.v, pr002_no_self_creation.v, pr004_no_two_step_giving.v.
• Proof found by the round-4 model (by cases): imkan_b_necessary_exists.v.
• Proofs found by the round-3 model, with Rocq check output: pr002_no_self_creation.v, pr004_no_two_step_giving.v, pr011_something_caused.v, kalima_first_cause.v, step3_possible_needs_cause.v.
• summary.csv: every evaluation run and its limits.
• heldout_round5_search_log.jsonl.gz: every step the round-5 model and the provers tried on the eight tasks, and Rocq's response, including the failed attempts on premises 1 and 3.
• heldout_round4_imkan_search_log.jsonl.gz: the same for the round-4 run on three tasks.
• heldout_best_search_log.jsonl.gz: the same for the round-3 model.
• Code: htps.py, rocq_env.py, run_eval.py, train.py, prep_data.py, gen_problems.py, filter_hard.py, gen_cuts.py, collect.py, collect_critic.py, gen_chains.py, hammer_heldout.py.