First Proof Batch 3: A Debrief

22 Oct, 2026

Mark Kim, with Zhengyang Zhang, Jing Xiong, Jui-Hui Chung, Hongzhou Lin, Xingyang Li, Junxian Guo, Enrico Shippole, and Ligeng Zhu

Overview

In October 2026, our team submitted the Humanize harness running Kimi K3 to First Proof Batch 3, a benchmark of unpublished research-level mathematics problems graded by expert referees. Our goal was to test how far an open-weight model, combined with an open-source agentic harness and optimized inference, could go on research-level mathematics. Our submission was the only one built on an open-weight model, and we served that model on our own stack rather than calling a provider’s API, so that we could control accuracy through our own choice of quantization and tune serving to the needs of a 24-hour run.

No solution was judged fully correct, but K3 made partial progress on several problems. On Problems 3, 5, and 7, it found the right overall approach or established special cases before its arguments broke down, and on Problem 5 the referees’ score of −0.5 is hard to reconcile with the rubric’s zero for an acknowledged partial result. For comparison, ProofCouncil, a harness built on GPT-6 Astra, solved nine of ten problems, and GPT-6 Astra on its own solved seven.

Serving K3 ourselves took substantial inference engineering. We sped up K3 2.3× on GH200 GPUs and by 44 percent over stock software on B300 GPUs. When our development cluster went down two days before the deadline, DeepInfra provided two nodes of eight B300s, and the run completed on October 2–3 within the 24-hour limit.

Figure 1. Batch 3 referee scores by problem and system, for correctness, exposition, and attribution. Source: First Proof [9].

The appendices hold the full harness configuration, serving measurements, run details and cost, and an AI-assisted assessment of the results.

Setup

First Proof gives every team the same ten unpublished research-level problems and runs each team’s code once, autonomously, in a Docker container on a CPU-only AWS instance, with a 24-hour limit for the whole container and at most 16 pages per solution [1, 2]. About 30 expert referees grade the solutions double-blind for correctness, exposition, and attribution. A wrong proof scores negatively on correctness, while a blank does not.

Eligible systems must call publicly available models through an API. We applied on September 9 with two configurations of the same harness, one running GPT-6 Astra and one running Kimi K3. The organizers wanted a more diverse set of models tested: they ranked our K3 entry, submitted alongside our Astra entry as an A/B pair, above a team on their waitlist, accepted both configurations as a single submission, and made an exception to the public-API rule for our self-served endpoint, on the condition that they have full access to our servers during the run. A team using a DeepSeek model had also applied but was not tested in the end, which left ours as the only open-weight submission. We and the organizers both expected Astra to outperform K3. On IMO and IOI, the Humanize team had first gotten each flow working with a frontier model before swapping in an open model, and the Batch 3 timeline compressed that process into a few weeks. The value of the K3 run was to show how far an open model with an open harness could go on research-level problems.

Our system is built on Humanize, an open-source harness that originated in the PolyArch Lab at UCLA and has since been developed with community contributors, including Ligeng’s team at NVIDIA and members of Song Han’s lab at MIT [3]. In its Ralph Loop with Codex Review (RLCR), run inside the OpenAI Codex CLI [4], a K3 worker writes each proof and a separate K3 reviewer either accepts it or returns findings for the next round. This was the earlier RLCR workflow, not the newer Humanize 2 flows, which add further verification such as fresh reviewer sessions. Because the Batch 2 solutions are public, we tested with web search and outside sources off, and the plan kept them off for Batch 3 to match, although the rules allowed them. Because wrong proofs score negatively, it also tells the model to report a genuine obstruction rather than invent a theorem or hide a gap [5]. If the loop had not accepted a proof by the deadline, the harness submitted its latest compiled draft, marked as incomplete. Zhengyang on our team adapted the harness for First Proof (Appendix A).

Testing on Batch 2

We developed the harness against the ten Batch 2 problems, with web access disabled [6]. An early parallel prover with GPT-6 Astra took two to three days on some problems, well over the limit. Codex alone and Codex with RLCR each produced internally accepted proofs for 9 of 10 problems within 14 hours. Referees did not grade these runs, so internal acceptance could not establish correctness, and we chose RLCR on this preliminary evidence (Appendix A). Because each round and its review must finish before the next begins, decoding speed sets how many rounds fit into 24 hours, so we spent most of our engineering time on serving.

Serving K3 ourselves

K3 is available through an API, but we chose to control the entire stack, because hosted open models perform differently across providers and a 24-hour run with ten long-context workers depends on decoding speed and prompt caching. K3 is a 2.8-trillion-parameter mixture-of-experts model whose experts ship in 4-bit MXFP4 [7]. Enrico set up K3 and the endpoint the First Proof container called, and tested that the full system ran end to end, while Xingyang and Junxian of the MIT HAN Lab led the optimization.

32 GH200s. We developed on JUPITER through a compute grant from the Jülich Supercomputing Centre. Our first deployment there served roughly 700 tokens/s in total across up to 128 concurrent connections, which was slow per user compared with commercial endpoints. Hopper GPUs have no 4-bit tensor cores, and four changes (speculative decoding, our own INT4 W4A8 compression, all-reduce tuning, and kernel fixes) took K3 from 15.1 to 34.1 tokens/s per user at 50 users, a 2.3× speedup. We released the checkpoint and our SGLang patches on Hugging Face [17].

8 B300s. On Blackwell, the situation reverses. Blackwell runs K3’s native weights directly, and stock SGLang reached 41.9 tokens/s per user on one node [8]. Our tuned 32 GH200s came within 8 tokens/s of that using four times as many GPUs. Three lossless settings that let speculative decoding pay off at high concurrency raised this to 60.2, 44 percent above stock (Figure 2, Appendix B). Xingyang and Junxian found those settings with a coding agent that read the SGLang source and public B300 reports before using any GPU time. These throughput figures come from AIME and HMMT benchmark requests at 50 concurrent users, not from the First Proof run itself, which sent five problems to each node.

Figure 2. Tuned GH200s against stock and tuned B300s.

The final 48 hours

Several of our collaborators were finishing ICLR submissions in the same weeks we were modifying the harness. On September 30, about 48 hours before our deadline, JUPITER went down for maintenance. We reached out to DeepInfra, and they were gracious enough to provide two nodes of eight B300s, better hardware than we had been using. They moved remarkably fast, and Enrico had K3 running on both endpoints, tested end to end, by the evening of October 1, the day the code was due. A final review of the code caught a configuration issue that would have stopped the run, Zhengyang fixed it within minutes, and we shared both repositories with the organizers that night.

We were up until 4 a.m., unable to sleep from the adrenaline. The organizers started the K3 run on the evening of October 2, and it completed in 20.2 hours, within the 24-hour limit, on two independent serving replicas with five problems each (Figure 3; Appendix C).

Figure 3. First Proof Batch 3 timeline.

Results

Results were published on October 14 [9]. No K3 solution was judged fully correct, but K3 made partial progress. On Problems 3, 5, and 7, it found the right overall approach or established special cases before its arguments broke down (Table 1).

Table 1. Kimi K3 results by problem. Correctness is the average referee score on a scale from −1 to 1, tallied from the published referee reports.

The review loop accepted six of the ten proofs, yet referees found major errors in all six, so the K3 reviewer passed proofs that human referees rejected. The four incomplete drafts also scored negatively on correctness; left blank, they would have scored zero. The referee reports describe failures that recur across problems: undefined terminology, citations to papers that do not exist, a conjecture presented as an established theorem, and conclusions that were not sanity-checked [14]. These failures were common across systems: in Batch 2, referees flagged citation problems, from uncredited borrowing to invented references, in 25 of 39 submissions, including from harnesses that checked citations [6]. The failures were not limited to problems that ran out of time. On Problem 4, K3 argued that its transition functions must be constant because the divisor is compact, although those functions are defined only on open overlaps, and its internal reviewer approved that step and declared the disproof correct. On Problem 8, K3 treated the Greenfield–Wallach classification, which is a conjecture, as an established theorem, and its reviewer certified the citation. In both cases the reviewer endorsed the worker’s false premise (Appendix D).

Batch 3 was designed to be harder than Batch 2: the organizers excluded any problem that GPT-5.6 Sol Pro solved in one attempt [1]. Table 2 compares the five tested systems. GPT-6 Astra, run on its own without an iterative harness, solved seven of ten problems for $36. First Proof estimated the API-equivalent cost of our run at about $2,127, from 716 million input and 15 million output tokens [14]. Because we served K3 ourselves, this is an estimated API price rather than an actual bill, and the comparison reflects differences in workflow as well as model, since our submission ran repeated rounds of proof generation and review. Appendix C gives token-based and hardware-based estimates.

Table 2. Batch 3 systems. Problems correct and costs are from First Proof; average correctness is tallied from the published referee reports.

To better understand the results, we used GPT-6 Astra to assist an assessment of the referee reports, K3’s submissions and internal reviews, and the released harness code, checking selected findings against the underlying records (Appendices D and E). The assessment found that Humanize largely executed its intended iterative workflow, but that K3’s reviewer repeatedly failed to catch mathematical errors. Several factors keep us from attributing these failures to the model alone. Two were deliberate choices: K3 served as both worker and reviewer, and outside sources were off to match our Batch 2 tests. The third was a gap in our adapter, which did not pass K3’s prior reasoning back to the model between turns; its effect has not been measured. The results therefore describe this specific model and harness configuration rather than K3’s capability on its own.

The Astra configuration and next steps

We also prepared the Astra half of the pair: the same Humanize harness running GPT-6 Astra [10]. After submission, the organizers decided not to run additional systems, citing the extra workload created by OpenAI’s data release, so the Astra configuration was not tested in Batch 3. That left a central question open: how much of the outcome came from the base model, and how much from the harness? The two existing runs cover only two of the four combinations in Table 3, and they were not matched on tool access. We also need to fix our Kimi adapter and measure that change on its own, so that it is not confused with a change of harness. We plan to complete the comparison ourselves on the released problems, running Humanize with GPT-6 Astra and K3 with its default harness under the same 24-hour limit (Table 3), and to score the runs with an AI grader calibrated against the published referee reports. Zhengyang will also rerun K3 with the upgraded harness, and the Humanize team will formalize the Batch 3 problems in Lean and attempt them with Humanize Prover.

Table 3. Planned runs on the Batch 3 problems

Reflections

A reviewer on the same model shares its blind spots. Our design assumed a strong, independent judge: when planning the harness, Jui-Hui proposed a GPT-6 Astra reviewer with fresh context, since in our experience Astra is a reliable judge of correctness. In the K3 configuration, K3 judged its own proofs. The K3 reviewer accepted six proofs that referees found wrong.

Under negative scoring, a blank beats a wrong draft. All four of our incomplete drafts scored negatively, where blanks would have scored zero. Siege made the opposite choice: it withheld two proofs its own solver had marked proved after a final scope check failed (Appendix E).

Is the extra cost of a harness worth the gain? This question goes beyond our own run, but Batch 3 raises it directly. GPT-6 Astra on its own solved seven of ten problems for $36. ProofCouncil, the strongest harnessed system, solved nine for $1,892, more than fifty times the cost for two more problems, and every harnessed system cost over $1,300 (Appendix C). Batch 2 showed the same pattern: a prompted GPT-5.5 Pro matched a harness built on the same model at a forty-first of the cost, and the strongest harness bought one more passing proof at 27 times the cost [6]. For hard research problems, two more correct proofs can easily be worth that, and we expect many teams to see it that way. Still, how large a cost multiple an accuracy gain justifies is worth asking, both for those building harnesses and for those paying for them.

Controlling the stack was worth the cost. Running K3 ourselves showed us where the time goes: on GH200s, almost half of each step was communication between GPUs; on B300s, the limit is reading the weights once per step.

Open-weight models need serving work that closed APIs hide. On Hopper, K3 needed custom compression, communication tuning, and kernel work to reach 34.1 tokens/s per user; on Blackwell, stock software reached 41.9 on a quarter of the GPUs. Results for open models on benchmarks like First Proof depend on this work as well as on the model.

Infrastructure risk falls hardest on small teams. A single maintenance window nearly cost us the submission. What saved it was a relationship with DeepInfra built before we needed it, and their willingness to act within a day.

Acknowledgments

We are grateful to DeepInfra for their support, and in particular to Pernekhan, Temirulan, and Nikola, who provisioned two nodes of eight B300s on a day’s notice when our cluster went down. Our submission would not have been possible without them.

We thank the Jülich Supercomputing Centre for the JUPITER compute grant. Zhengyang Zhang built and tested the First Proof harness, Ligeng Zhu and the Humanize team developed Humanize (which originated in the PolyArch Lab at UCLA), Jui-Hui Chung advised on harness design, Jing Xiong and Hongzhou Lin provided feedback on the design, Enrico Shippole deployed K3, set up the endpoint, and tested it end to end, and Xingyang Li and Junxian Guo of the MIT HAN Lab optimized its serving.

Sources

1. First Proof Editorial Board. “Third Batch Call for Submissions.” August 25, 2026. https://1stproof.org/assets/docs/batch3-call-for-submissions.pdf
2. First Proof. “First Proof Benchmarking Protocol, Batch 3.” Provided to submitters, September 2026.
3. PolyArch. “Humanize.” GitHub repository, commit fc0e0be. https://github.com/PolyArch/humanize
4. OpenAI. “Codex CLI,” version 0.157.1. GitHub repository. https://github.com/openai/codex
5. Humanize RLCR, Kimi K3/max. First Proof Batch 3 submission repository, October 2026. Private; available on request. https://github.com/markykim/first-proof-3kimi
6. First Proof. “Second Batch.” Accessed October 21, 2026. https://1stproof.org/second-batch.html
7. Xingyang Li and Junxian Guo. “Serving Kimi-K3 for First Proof: What We Changed on 32 GH200s and 8 B300s, and What We Measured.” MIT HAN Lab, October 8, 2026.
8. SGLang. GitHub repository. https://github.com/sgl-project/sglang
9. First Proof. “Third Batch.” October 14, 2026. https://1stproof.org
10. Humanize RLCR, GPT-6 Astra/max. First Proof Batch 3 submission repository, October 2026. Private; available on request. https://github.com/markykim/first-proof3
11. Zhengyang Zhang, Jing Xiong, Hongzhou Lin, Jui-Hui Chung, Zijian Zhang, Song Han, Sihao Liu, and Ligeng Zhu. “Humanize Olympiad Agents (HOA): A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify.” arXiv:2610.13632, 2026. https://arxiv.org/abs/2610.13632
12. Yuan Liao, Ziyang Qin, Jui-Hui Chung, Ayush Khaitan, Zhengyang Zhang, Hongzhou Lin, Zijian Zhang, Ligeng Zhu, Peng Lu, and Bennett Chow. “A Lean Formalization of the Hamilton–Perelman Proof of Thurston’s Geometrization Conjecture.” arXiv:2610.13897, 2026. https://arxiv.org/abs/2610.13897
13. First Proof. “First Proof Third Batch: Press Release.” October 14, 2026. https://1stproof.org/third-batch-press-release.html
14. First Proof. “batch-3.” GitHub repository with referee reports, costs, and raw outputs. Accessed October 21, 2026. https://github.com/1stproof/batch-3
15. Moonshot AI. “Kimi K3 Is Here: Our Most Capable Model.” Moonshot AI Forum, July 22, 2026. https://forum.moonshot.ai/t/kimi-k3-is-here-our-most-capable-model/480
16. DeepInfra. “Pricing.” Accessed October 21, 2026. https://deepinfra.com/pricing
17. Xingyang Li and Junxian Guo. “Kimi-K3-W4AFP8.” Hugging Face model repository, October 2026. https://huggingface.co/Radioheading/Kimi-K3-W4AFP8
18. Ivo Petrov, Jasper Dekoninck, and Martin Vechev. “BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs.” arXiv:2510.04721, 2025. https://arxiv.org/abs/2510.04721

Appendix A. Harness details and Batch 2 tests

Background on Humanize. Humanize was built with the perspective that, given the same model and the same tokens, the flow that organizes the model’s work accounts for much of the difference in results. The first version is the single RLCR loop described above. Humanize 2 turns it into a framework for writing a different flow for each kind of task. Its first large application, Humanize Olympiad Agents (HOA), adds a structured wiki of task-specific knowledge and a verifier that checks Lean proofs against trusted statements, and accepts an answer only after every review and verification gate passes [11]. HOA reported full or near-full marks on the 2026 IMO, IPhO, IOI, and IChO, solved all 672 PutnamBench problems, and ranked first on the Lean-Eval leaderboard. Most relevant to our submission, Kimi K3 with HOA matched GPT-5.6 Sol on the olympiads, and most of K3’s gains came from the harness rather than the model (Table A1).

Table A1. Results reported for HOA by the Humanize team

Recent formalization. The same group has since moved from competition problems to research mathematics. In October 2026, a team including Zhengyang, Jui-Hui, Zijian Zhang, Hongzhou Lin, and Ligeng, working with the Ricci-flow specialists Peng Lu and Bennett Chow, released a Lean formalization of the Hamilton–Perelman proof of Thurston’s geometrization conjecture, which contains the Poincaré conjecture as a special case [12].

Every problem received the same plan, with five acceptance criteria: answer every part of the question, stay self-contained relative to graduate-level mathematics, audit the proof for quantifiers, degenerate cases, and constants, give a rigorous disproof or diagnosis if the statement is false, and produce a standalone LaTeX file within 16 pages. Although the rules allowed web access, the plan forbids web search, browsing, subagents, and outside sources, matching the conditions under which we tested. It also states that “honest identification of a genuine obstruction is preferable to an invented theorem or concealed gap” [5]. Given the negative scoring for wrong proofs, this instruction was deliberate.

Codex speaks OpenAI’s Responses protocol, while our K3 servers spoke Chat Completions. We wrote a small bridge, running only inside the container, that translates requests, tool calls, and token counts between the two. It contains no model logic; K3 does all of the proof and review work.

All ten problems ran at once, five on each serving node. At the end, the harness compiles each solution to PDF and checks the page count. If a problem had not reached an accepted state by the shared deadline, the harness submitted the latest draft that compiled and fit the page limit, marked as incomplete; a problem was left blank only when no such draft existed. Table A2 summarizes the configuration.

Table A2. Harness configuration for the K3 submission

Batch 2 tests

We developed the harness against the ten problems from First Proof’s second batch, with web access disabled [6]. The strongest Batch 2 system, ProofCouncil from ETH Zurich, had solved 6 of the 10. Zhengyang first tried GPT-6 Astra in a DAG-style parallel prover, similar to the Goedel-Prover design, which breaks a proof into dependent pieces and works on them in parallel. It solved the problems it finished, but individual problems took two to three days, well over the 24-hour limit (Table A3, Figure A1).

Table A3. Wall time per Batch 2 problem in an early parallel run with GPT-6 Astra

Zhengyang then compared three flows inside Codex: Codex alone, Codex with RLCR, and Codex with a decomposition step (Table A4). Codex alone and Codex with RLCR each finished 9 of 10 problems within 14 hours. The decomposition flow also reached 9 of 10 but needed more time, in part because it ran a review on the decomposition itself; without that review it finished 4 of 10 in seven hours, with four more close. Here “finished” means the flow’s own reviewer accepted a proof. These results were not graded against referee reports, and Jui-Hui pointed out that a fresh session should judge each proof before we count it as solved. We chose RLCR for the submission.

Table A4. Batch 2 test results by flow

Figure A1. Batch 2 wall time per problem in an early parallel run with GPT-6 Astra, against the 24-hour limit.

One change between our two configurations shows a trade-off we weighed. Our Astra harness submitted a blank whenever the review loop had not accepted a proof. For K3, which decodes more slowly and was less likely to finish every loop within 24 hours, we chose to submit the latest compiled draft instead, labeled as incomplete.

Appendix B. Serving details

K3 is available through an API, but we chose to control the entire stack. Hosted open models can perform differently across providers, depending on quantization and batch size. A 24-hour run with ten long-context workers depends on decoding speed and on how often the server can reuse cached prompts between rounds, and we wanted to set precision, caching, and scheduling ourselves. Because First Proof runs each container on a CPU-only instance, K3 also had to sit behind an endpoint reachable from AWS for the full 24 hours. K3 is a 2.8-trillion-parameter mixture-of-experts model whose experts ship in 4-bit MXFP4 [7]. Enrico set up K3 and the endpoint the First Proof container called, and tested that the full system ran end to end, while Xingyang and Junxian of the MIT HAN Lab led the optimization. We measured output tokens per second per user, the median over requests including queueing and prefill, on AIME 2026 and HMMT 2026 problems with 20 or 50 users at once.

32 GH200s. We developed on eight nodes of four GH200 GPUs on JUPITER, through a compute grant from the Jülich Supercomputing Centre. Hopper GPUs also have no 4-bit tensor cores, and K3 needs substantial changes to run well on them. The W4A8 path did not run at all until we rebuilt SGLang’s kernel library with sm_90a support, which the aarch64 build had left out. The baseline configuration (TP4 × PP8, no speculative decoding) reached 15.1 tokens/s per user at 50 users. Four changes, each measured on its own, brought this to 34.1 tokens/s, a 2.3× speedup (Table B1, Figure B1). Our own INT4 W4A8 compression, with INT4 weights, FP8 activations, and an activation-aware scale for each group of 128 weights, had 17 percent lower KL divergence from the native model than the public W4AFP8 checkpoint, and kept math accuracy within noise of the native model (81.3 versus 82.3 percent). All-reduce took 48 percent of each step before NCCL tuning cut it by a third. Without requantizing, the native weights with a fix to the Marlin MoE kernel’s tiling reached 29.6 tokens/s per user with KL divergence at the noise floor, and two W4A8 replicas on 64 GPUs reached 35.7. We released the W4A8 checkpoint, with the SGLang patches and launch command, on Hugging Face as Radioheading/Kimi-K3-W4AFP8.

Table B1. K3 output speed on 32 GH200s at 50 users, adding one change at a time

Figure B1. K3 output speed on 32 GH200s as each change is added.

8 B300s. On Blackwell, the situation reverses. B300s run MXFP4 weights with MXFP8 activations natively, so we served the official checkpoint without requantizing, and thanks to the SGLang team, stock SGLang already serves K3 well on them [8]. One node of eight B300s reached 41.9 tokens/s per user at 50 users. Our tuned 32 GH200s came within 8 tokens/s of that number using four times as many GPUs. Our contribution on the B300s was to make speculative decoding pay off at high concurrency. In the public B300 configuration, speculation was slower than no speculation above 16 users. Under speculative decoding, SGLang silently caps running requests at 48, so at 50 users the verification step fell outside the captured CUDA graphs, which we believe explains the public result. Three settings fixed this: a request cap of 64 instead of 48, a CUDA-graph batch size of 64 so verification stays in-graph, and a draft block of 3 tokens instead of 7. With them, one node reached 60.2 tokens/s per user at 50 users, 44 percent above stock, and 87.8 tokens/s at 20 users, twice our best GH200 result (Figure 2). All settings were lossless, with a BF16 KV cache and exact verification. Xingyang and Junxian found these settings in about two hours with a coding-agent workflow: it read the SGLang source and public B300 reports before using any GPU time, measured each change on real AIME and HMMT prompts, and fitted a step-time model from server logs to rule out whole sweeps without running them.

The ceiling on one node. Each decoding step reads every weight once, which costs a fixed 25.6 ms (about 195 GB per GPU), plus 0.089 ms for each verified token. At 2.3 accepted tokens per step, one node tops out near 90 tokens/s per user, and draft blocks of 2, 3, or 4 tokens perform within 3 percent of one another (Figure B2). Splitting the model across both nodes with TP16 would halve the fixed cost, but the nodes were connected by Ethernet rather than InfiniBand. We therefore ran two independent TP8 replicas, one per node, each serving five problems.

Figure B2. Time per decoding step on one B300 node.

Appendix C. Run details and cost

The container ran for 20.2 hours, within the 24-hour limit. In total, the system read about 716 million input tokens and generated about 15 million output tokens, which First Proof priced at about $2,127 [14]. As the protocol requires, the harness logged input, cached-input, output, and hidden reasoning tokens for every worker and reviewer call [2]. Results were published on October 14, and ours was the only submission built on an open-weight model [9].

Figure C1. Input tokens per problem in the Batch 3 run, by harness status.

Batch 3 was designed to be harder than Batch 2, to keep pace with improving models. The organizers excluded any problem that GPT-5.6 Sol Pro solved in one attempt during preliminary testing, and they allowed problems whose human proofs run up to 12 pages, up from 8 in Batch 2 [1]. The stated aim was to keep the benchmark at the edge of AI capability: excluding problems the best model could solve in August would focus it on problems likely to remain hard for models in October [1]. Table 2 compares the five tested systems. The organizers also compared our system with older frontier models and judged it generally less capable than GPT-5.2 Pro, the leading frontier model in December 2025 [13].

Because we served K3 on rented hardware, there was no API bill for our run, and First Proof estimated its cost [14]. The $2,127 figure applies DeepInfra’s Kimi K3 API prices to our logged tokens and counts 6.8 percent of input tokens as cached, the share our server reported from its prefix cache; the harness’s own log recorded no cached tokens. First Proof also estimated the hardware cost at about $1,960 for roughly 400 GPU-hours on 16 GPUs. That works out to $4.90 per GPU-hour, which matches DeepInfra’s listed B200 rate of $4.89 rather than its B300 rate of $5.89 [16]. Table C1 recomputes both estimates at the list prices published by Moonshot and DeepInfra [15, 16].

Table C1. Cost of our run at list prices. Token costs use 715.6 million input tokens, of which 48.7 million are cached in the 6.8 percent case, and 15.0 million output tokens.

Cost of the closed-model systems. The cost comparison favors the simplest system. GPT-6 Astra, run by OpenAI as a single prompt with no harness, solved seven of ten problems for $36 in total, about $5 per correct solution. ProofCouncil solved two more for $1,892, about $210 per correct solution, and the cheapest harnessed system, Siege, cost $1,321 (Table 2). On this batch, a single call to a strong closed model delivered most of the frontier result for under 3 percent of the cost of any harnessed system, while our run cost about $2,127 and solved none.

Appendix D. AI-assisted assessment of the Batch 3 results

This appendix summarizes an assessment generated with GPT-6 Astra from the published Batch 3 materials [14]. It examined the individual referee reports, K3’s submitted proofs and internal reviews, the harness code, and selected competing and human solutions, and it checked several failures directly. It did not re-certify all fifty proofs. Its categories for each system come from the individual referee reports rather than from averaged scores. We checked the specific claims about Problems 4, 5, 7, and 8 below against the repository.

Table D1. Assessment of each system from the individual referee reports

Table D2. K3’s submission by problem, with the strongest comparison

Problem 4. K3 argues that holomorphic transition functions on overlaps must be constant because the divisor is compact. Those functions are defined on open overlaps, not globally on the compact divisor, so the step fails. Its proposed counterexample is a projective line in CP², where the standard complex structure already supplies the required local holomorphic coordinates. On two standard charts the normal defining functions satisfy z′ = z/w, so the transition function 1/w varies along the overlap. K3’s internal reviewer approved the constant-transition step, declared the disproof correct, and marked the problem complete. The worker and the reviewer made the same error.

Problem 7. K3 defines a map on an annulus by h(w) = e^{iθ(|w|)}·w, with θ = π near the outer boundary, and sets h equal to the identity outside the annulus. Just inside that boundary the map is w ↦ −w, and just outside it is w ↦ w, so the pieces do not join continuously, although the proof claims they define a homeomorphism. This can be checked without the surrounding dynamics.

Problem 8. The proof moves its main difficulty into a supposed Greenfield–Wallach theorem, and K3’s internal reviewer certified it as a real, correctly cited result. The human solution and the referee identify the relevant classification as a conjecture, so the averaging and entropy arguments that follow rest on an unproved input.

Pattern. In each of these cases, the system accepted a false simplifying premise and then built extensive reasoning and review around it. Frontier models show the same tendency: on BrokenMath, a benchmark of plausible but false theorems, GPT-5 produced proofs of false statements 29 percent of the time [18].

Competing submissions. ProofCouncil’s proof for Problem 2 reaches the exact rate without the logarithmic loss in the human solution. Its proof for Problem 8 builds a nonsmooth invariant distribution from positive entropy instead of assuming the desired rigidity, and its proof for Problem 10 uses lattice structure to simplify the construction. GPT-6 Astra found the central pinching and unpinching mechanism on Problem 9, which ProofCouncil missed, so the strongest system overall did not lead on every problem.

Qualifications. The assessment notes five limits on the comparison. First, our harness disabled web search and outside sources, while Astra’s trace shows searches and paper retrieval; this bears on the theorem-status and citation failures, though not on the elementary errors in Problems 4 and 7. Second, incomplete runs explain only part of the result, since Problems 4, 6, 8, and 10 were marked complete. Third, on Problem 5 both referees scored K3’s acknowledged partial result at −0.5, while the rubric gives zero for acknowledged partial work; this affects the average but would not turn the submission into a solution. Fourth, some favorable reports on other systems say that not every computation could be checked in the time allowed. Fifth, the worker logs for K3’s Problems 6 to 10 were not released, which limits reconstruction of those failures.

Recommendation. The assessment recommends improving verification before running longer: require the system to retrieve any theorem its argument depends on, test proposed counterexamples and obstructions against elementary cases, and compare review by K3 alone with review by a stronger external model under matched conditions. Adding review rounds does not help when the reviewer shares the worker’s central mistake and endorses it.

Follow-up clarification. A second pass of the same assessment corrected parts of its first reading. Humanize is designed as an iterative builder and reviewer loop: work against acceptance criteria, receive criticism, revise, and stop when the work is accepted or the loop stops making progress [3]. Several behaviors the first pass treated as defects are part of that design or of choices we made for the submission (Table D3).

Table D3. Harness behavior in the Batch 3 run: first reading and revised interpretation

The acceptance criteria were also stronger than a compile check. The submitted plan required complete proofs, precise theorem applications, checks of quantifiers and edge cases, and no conjectures presented as established results [5]. The failure was that K3’s reviews sometimes judged those requirements satisfied when they were not. The submission also pinned one commit of PolyArch’s Humanize; the current Humanize runtime from Humanfia supports a broader set of flows, including fresh reviewer sessions, which this run did not test.

The revised conclusion is that Humanize largely executed its intended workflow, but K3’s mathematical judgments within it were unreliable on these problems. Whether the loop improved on K3 alone, and whether another model would fail the same way, can only be settled by matched comparisons.

Appendix E. Harness code of the released submissions

A second pass of the assessment read the execution, review, stopping, and export code of the four released harnesses (Humanize with K3, ProofCouncil, Siege, and MerLean) and checked it against the released run artifacts [14]. For the standalone Astra run, whose harness source was not released, it inspected request settings and traces. It did not rerun any model or audit every line of code. The comparison is between complete systems, so it does not rank the underlying models. We checked the run statuses, stopping points, and withheld answers below against the released files.

Table E1. What each released harness implements

Export policy. Our wrapper’s export condition in run.py is valid standalone LaTeX, a successful compile, and the page limit [5]. Acceptance by the review loop changes the recorded status but is not required for export, so four unfinished drafts were submitted (Table E2). Two of them, Problems 3 and 5, ended at Humanize’s circuit breaker after three consecutive reviews judged the run stalled. Problem 5 stopped after 8.3 hours, with up to 42 review rounds allowed. The unfinished drafts account for four of the ten failures. They do not account for the six invalid proofs the loop accepted.

Table E2. Humanize run status by problem

Review at the point of failure. On Problem 4 the internal review approved the exact step that fails and certified the proof (Appendix D). The workflow gives the reviewer substantive mathematical instructions, but the loop advances through Codex’s generic review command, which lets a round pass when it returns no priority-tagged findings [4]. That machinery was built for software review and gives no guarantee of mathematical correctness.

ProofCouncil. The recorded run used one author per problem, although a multi-author preset was available, and its usage logs show cross-model consultation. The features that plausibly explain its stronger results sit in its author and critic workflow and its publication logic: periodic fresh critics, with a fresh review required before acceptance whenever a long-running critic agrees; accepted versions tracked by hash; a newly found flaw able to revoke an earlier acceptance; and deadline output kept separate from accepted solutions. These target two failure modes, shared assumptions building up across rounds and edits that invalidate an earlier review. The run does not isolate how much each contributed.

Siege. Its runner separates solving, checking that the proof answers the question as posed, and checking that the LaTeX write-up is faithful. In the released results, Problems 3 and 4 reached an internal PROVED verdict and passed the ledger gate, yet were withheld because the final scope check did not confirm that the proof settled the problem as posed. Some of Siege’s blanks are therefore answers its own checks rejected.

MerLean. Its manuscript review checks reviewer separation, manuscript hashes, unresolved findings, and correspondence with the original question, and the final review asks for verification of essential cited claims. The run used the Lite workflow, so its answers were not certified in Lean. It recorded Problems 3, 4, 6, 8, and 9 as scope-blocked while still exporting their sources. Its results show that added review stages are not enough by themselves. The full 22 GB working output was not released, which limits reconstruction of its research process.

Conclusion. ProofCouncil combined the strongest mathematical output with the most disciplined acceptance. Siege showed useful restraint, and MerLean showed that elaborate review can still leave large gaps. Our K3 run showed both false acceptance and early stopping followed by draft export. The code leaves K3’s incorrect mathematics standing, and it also undercuts any claim that K3 is inherently incapable. A fair capability comparison would hold the harness, web access, budget, and reviewer policy fixed, after fixing how our adapter handles K3’s prior reasoning.