The Obfuscated Natural Number Game: Are LLM Provers Reasoning or Memorizing?
> Paper: Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game > Author: Lixing Li > arXiv: 2605.00677 | 2026-04-30
1. The "Math Genius" Who Memorized the Answers
Imagine a student who scores full marks in a math competition — but you suspect they may have simply memorized every answer. How do you test this?
- Give them new problems? They may have seen similar ones.
- Change the numbers? They may have grasped the pattern.
- Rename the mathematical concepts — call addition "merging" and multiplication "repeated merging" — and see whether they can still reason?
- Test problems may appear in training data
- Even if not, similar problem patterns may have been seen
- No way to distinguish "reasoning" from "memorization"
add→f1mul→f2succ→g- ... 3. Preserve the logical structure of all axioms and definitions 4. Ask the LLM to complete proofs in this obfuscated environment
- It remembers "use
add_commto prove this" - But
add_commhas been renamed to, say,f7 - It cannot invoke the theorem — the proof fails
- It understands the content of commutativity of addition
- Even named
f7, it can derive it from axioms — or at least recognize "commutativity is needed here" - The proof can continue
If they truly understand, they should handle renaming. If they only memorized, they will be confused.
2. The Genuine-vs-Fake Debate Over LLM Math Ability
LLMs achieve impressive scores on formal mathematics benchmarks like MiniF2F. But the key question: does this success come from genuine logical reasoning, or semantic pattern matching from training data?
Limitations of existing benchmarks:
What is needed: evaluation that tests what an LLM can *derive* from known axioms and definitions — not what it "knows."
3. The Obfuscated Natural Number Game as a Litmus Test
The paper proposes the Obfuscated Natural Number Game:
> Rename all identifiers in Lean's Natural Number Game (an interactive theorem-proving tutorial) and test whether an LLM can still complete the proofs.
The procedure:
1. Take Lean's Natural Number Game 2. Replace all identifiers (function names, theorem names, variables) with meaningless symbols:
What it tests: Does the LLM understand the *structure* of natural numbers (e.g., Peano axioms), or did it merely memorize theorem names and proof steps? Can it reason from first principles under unfamiliar symbols?
4. Why the Obfuscation Test Works
If the LLM only memorized:
If the LLM genuinely reasons:
5. The Feynman-Style Judgment: Understanding Means Applying in Unfamiliar Settings
Feynman said: "Knowing the name of something and understanding something are very different."
In mathematical reasoning: knowing a theorem's name and proof steps is not understanding. True understanding means you can rebuild everything from first principles even when every name has changed.
The philosophy of the obfuscation test: strip away all surface-level memorization and test deep understanding. Names and symbols may change, but the logical structure does not — and a genuine reasoner can work in any symbol system.
6. Takeaways
If you evaluate or use LLM reasoning, ask yourself:
1. Does my test distinguish "memorization" from "reasoning"? 2. Can the LLM still derive results under unfamiliar symbols/concepts? 3. Have I tested "reasoning from first principles"? 4. Is the evaluation rigorous enough to exclude training-data contamination?
Core insight: evaluating AI reasoning requires tests that rule out "memorization cheating." The Obfuscated Natural Number Game offers an elegant solution: change nothing about the mathematics, only the representation. If the AI can still reason, it truly understands; if not, it is a sophisticated memorizer.
As AI mathematical capabilities advance rapidly, distinguishing genuine from superficial understanding matters more than ever.