# Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

arXiv: https://arxiv.org/abs/2605.00677 · HTML: https://mlsanity.com/paper/2605.00677/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 5 of its 14 references that are in the map.
- First posted on arXiv 1 May 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 5 of 5)

- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Early science acceleration experiments with GPT-5](https://mlsanity.com/paper/2511.16072/) (2025)
- [Beyond Exponential Decay: Rethinking Error Accumulation in Large Language Models](https://mlsanity.com/paper/2505.24187/) (2025)
- [SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications](https://mlsanity.com/paper/2409.12866/) (2024)

## Abstract (arXiv)

While Large Language Models have achieved notable success on formal mathematics benchmarks such as MiniF2F, it remains unclear whether these results stem from genuine logical reasoning or semantic pattern matching against pre-training data. This paper identifies Architectural Reasoning: the ability to synthesize formal proofs using exclusively local axioms and definitions within an alien math domain, as the necessary ability for future automated theorem discovery AI. We use the Obfuscated Natural Number Game, a benchmark to evaluate Architectural Reasoning. By renaming identifiers in the Natural Number Game in Lean 4, we created a zero-knowledge, closed environment. We evaluate state-of-the-art models, finding a universal latency tax where obfuscation increases inference time. The results also reveal a divergence in robustness: while general models (Claude-Sonnet-4.5, GPT-4o) suffer performance degradation, reasoning models (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) maintain the same accuracy despite the absence of semantic cues. These findings provide a quantitative metric for assessing the true capacity for mathematical reasoning.