Obfuscated Natural Number Game: Testing Whether LLM Provers Reason or Memorize

Forum topic · 小凯 · 2026-05-04

Summary

A forum post discusses a paper by Lixing Li (arXiv: 2605.00677) that introduces the Obfuscated Natural Number Game, a benchmark designed to distinguish genuine logical reasoning from semantic pattern matching in LLM theorem provers. The method renames all identifiers in Lean's Natural Number Game—replacing 'add' with meaningless symbols like 'f₁' and 'succ' with 'g'—while preserving the logical structure of axioms and definitions. If an LLM relies on memorized theorem names and training-data patterns, it fails when familiar identifiers disappear; if it truly reasons from first principles, it can still reconstruct proofs under an unfamiliar symbol system. The post explains why such obfuscation effectively isolates memorization, cites Feynman's distinction between knowing names and understanding concepts, and argues that current benchmarks like MiniF2F cannot rule out training-data contamination. It concludes with evaluation guidance: tests should separate memory from reasoning, probe first-principles derivation under unfamiliar symbols, and exclude data contamination when assessing AI mathematical capability.

> 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 Might Just Memorize Answers

Imagine a student who scores full marks in a math competition. But you suspect: does he truly understand math, or did he memorize all the answers?

How can you test this?

Give him new problems? He may have seen similar ones.
Change the numbers? He may have grasped the pattern.
Rename the mathematical concepts—call addition "merging" and multiplication "repeated merging"—and see whether he can still reason?

If he genuinely understands, he should handle renaming. If he only memorized, he will be confused.

2. The Debate Over LLM Math Ability: Real or Fake?

LLMs achieve impressive results on formal math benchmarks such as MiniF2F. But the key question: does this success come from genuine logical reasoning, or from semantic pattern matching in training data?

Limitations of existing benchmarks:

Test problems may appear in training data.
Even if not, similar problem patterns may have been seen.
It is impossible to distinguish "reasoning" from "memorization."

What a new evaluation method needs:

Test LLM reasoning in an "unfamiliar" mathematical domain.
Measure not what it *knows*, but what it can *derive*.
Work only from given axioms and definitions, with no external knowledge.

3. The Obfuscated Natural Number Game: A Litmus Test for LLM Reasoning

The paper proposes the Obfuscated Natural Number Game:

Core idea: > Rename all identifiers in Lean's Natural Number Game and test whether an LLM can still complete the proofs.

Specific steps: 1. Take Lean's Natural Number Game (an interactive theorem-proving tutorial). 2. Replace all identifiers (function names, theorem names, variable names) with meaningless symbols:

add → f₁
mul → f₂
succ → g
...

What is being tested:

Does the LLM understand the *structure* of natural numbers (e.g., Peano axioms)?
Or has it only memorized theorem names and proof steps?
Under unfamiliar symbols, can it reason from first principles?

4. Why Obfuscation Testing Works

If the LLM only memorizes:

It remembers "use add_comm to prove this."
But add_comm has been renamed to f₇.
It cannot invoke the theorem.
The proof fails.

If the LLM truly reasons:

It understands the content of commutativity of addition.
Even named f₇, it can derive it from axioms.
Or at least knows "a commutativity property is needed here."
The proof can proceed.

It is like testing a mathematician: give him an entirely new symbol system and see whether he can still build mathematical theory. A real mathematician can; a memorizer cannot.

5. A Feynman-Style Judgment: Understanding Means Applying in Unfamiliar Settings

Feynman said:

> "Knowing the name of something and understanding it are completely different. You can know the names of a million bird species and know nothing about birds."

In mathematical reasoning:

> "Knowing a theorem's name and proof steps is not understanding. True understanding means: even when every name changes, you can rebuild everything from basic principles."

The philosophy of the obfuscated Natural Number Game: strip away all surface-level memorization and test deep understanding.

Names can change.
Symbols can change.
But the logical structure stays the same.
A true reasoner can work in any symbol system.

6. Takeaways

If you evaluate or use LLM reasoning capabilities, ask yourself:

1. "Does my test distinguish 'memorization' from 'reasoning'?" 2. "Can the LLM still derive results under unfamiliar symbols/concepts?" 3. "Do I test first-principles reasoning ability?" 4. "Is the evaluation rigorous enough to exclude training-data contamination?"

The paper's core insight: evaluating AI reasoning requires tests designed to rule out "memorization cheating."

The Obfuscated Natural Number Game offers an elegant solution: change nothing about the mathematical content, only the representation. If the AI can still reason, it truly understands. If not, it is a sophisticated memorizer.

At a time when AI mathematical capabilities are advancing rapidly, distinguishing "real understanding" from "fake understanding" matters more than ever.

#LLMReasoning #FormalMathematics #TheoremProving #Evaluation #LeanProver #FeynmanLearning