MaxProof lets one model exceed human gold-medal scores on IMO 2025 and USAMO 2026 by running tournament selection over populations of candidate proofs at test time.

Constructions for𝑘=0,1,3 *𝑘=0.Take the𝑛vertical lines𝑥=1,2, . . . , 𝑛. Every(𝑎, 𝑏) ∈𝑆 𝑛 lies on𝑥=𝑎, so all points are covered. None of these lines is sunny (all are vertical). *𝑘=1.For𝑛≥3take the vertical lines𝑥=1,2, . . . , 𝑛−1and the sunny line through(𝑛,1)and(1,2). Its slope is 1−2 𝑛−1 =− 1 𝑛−1, which is never0,∞or−1; hence it is sunny. The vertical li...

Boundary points and a lemma The set𝑆 𝑛 is a right-angled isosceles triangle with vertices(1,1),(1, 𝑛),(𝑛,1). Its boundary consists of three edges: 34 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling 𝐸1 :𝑥=1,1≤𝑦≤𝑛, 𝐸2 :𝑦=1,1≤𝑥≤𝑛, 𝐸3 :𝑥+𝑦=𝑛+1,1≤𝑥, 𝑦. Each edge contains𝑛lattice points, and the three corn...

Base case𝑛=3.𝑆 3 ={(1,1),(1,2),(1,3),(2,1),(2,2),(3,1)}

Inductive step We prove by induction on𝑛that the only possible values of𝑘are0,1,3. Base case𝑛=3.𝑆 3 ={(1,1),(1,2),(1,3),(2,1),(2,2),(3,1)}. The constructions above show that 𝑘=0,1,3are attainable. It remains to prove that𝑘=2is impossible. Assume, for contradiction, that there are three distinct lines covering𝑆3 with exactly two sunny lines. Let 𝐿be the un...

Therefore the set of admissible𝑘is {0,1,3}

Conclusion We have exhibited explicit constructions for𝑘=0,1,3for every𝑛≥3, and we have shown that no other non-negative integer𝑘can be realized. Therefore the set of admissible𝑘is {0,1,3} . 36 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling IMO 2025 Problem 2 (Self-Pick: 7/7) Problem Statement LetΩa...

2025

Place𝑀=(0,0), 𝑁=(1,0)and let the radii be𝑟 < 𝑅

Coordinate set-upThe problem is invariant under scaling, translation and rotation. Place𝑀=(0,0), 𝑁=(1,0)and let the radii be𝑟 < 𝑅. Then Ω:𝑥 2 +𝑦 2 =𝑟 2,Γ:(𝑥−1) 2 +𝑦 2 =𝑅 2. The line𝑀 𝑁(the𝑥-axis) meetsΩat𝐶=(−𝑟,0)andΓat𝐷=(1+𝑅,0); the order𝐶, 𝑀, 𝑁, 𝐷is satisfied because−𝑟 <0<1<1+𝑅. The two intersection points of the circles are 𝐴=(𝑥 0, 𝑦0), 𝐵=(𝑥 0,−𝑦 0), 𝑥 ...

Write𝑃=(𝑥 𝑃, 𝑦𝑃)with𝑦 𝑃 unknown

Circumcenter𝑃of△𝐴𝐶 𝐷 Since𝐶, 𝐷lie on the𝑥-axis, the perpendicular bisector of𝐶 𝐷is the vertical line through the midpoint of 𝐶 𝐷; hence 𝑥𝑃 = −𝑟+ (1+𝑅) 2 = 1+𝑅−𝑟 2 . Write𝑃=(𝑥 𝑃, 𝑦𝑃)with𝑦 𝑃 unknown. The condition𝑃 𝐴=𝑃𝐶(both equal to the circumradius) gives (𝑥 𝑃 −𝑥 0)2 + (𝑦 𝑃 −𝑦 0)2 =(𝑥 𝑃 +𝑟) 2 +𝑦 2 𝑃 . Expanding and using𝑥2 0 +𝑦 2 0 =𝑟 2 yields −2𝑥 𝑃 𝑥0 −2...

For a circle with centre𝑂and a point𝐴on it, the second intersection of the line𝐴+𝑡vwith the circle is obtained from|𝐴+𝑡v−𝑂| 2 =𝑅 2

The points𝐸and𝐹 Letv=𝑃−𝐴and set𝐴𝑃=|v|. For a circle with centre𝑂and a point𝐴on it, the second intersection of the line𝐴+𝑡vwith the circle is obtained from|𝐴+𝑡v−𝑂| 2 =𝑅 2. Since|𝐴−𝑂| 2 =𝑅 2, we get 2𝑡v· (𝐴−𝑂) +𝑡 2|v| 2 =0=⇒𝑡=− 2v· (𝐴−𝑂) |v| 2 . Thus the signed distance from𝐴to that second point along the directionu=v/|v|is 𝑠=𝑡|v|=−2u· (𝐴−𝑂). 37 MaxProof: S...

Inthecoordinate system with origin at𝐴, axes alongu(the𝑢-axis) andw(the𝑤-axis), we have 𝐴=(0,0), 𝐸=(𝑒,0), 𝐹=(𝑓 ,0), 𝐵=(𝑏, ℎ), where 𝑏=(𝐵−𝐴) ·u, ℎ=(𝐵−𝐴) ·w

Orthonormal basis aligned with𝐴𝑃 Letu=v/𝐴𝑃andletwbetheunitvectorobtainedbyrotatingu90 ◦ counter-clockwise. Inthecoordinate system with origin at𝐴, axes alongu(the𝑢-axis) andw(the𝑤-axis), we have 𝐴=(0,0), 𝐸=(𝑒,0), 𝐹=(𝑓 ,0), 𝐵=(𝑏, ℎ), where 𝑏=(𝐵−𝐴) ·u, ℎ=(𝐵−𝐴) ·w. First compute 𝑥𝑃 −𝑥 0 = (1+𝑅−𝑟) − (1+𝑟 2 −𝑅 2) 2 = 𝑌(1+𝑋) 2 = 𝑌𝑇 2 , 𝑦𝑃 −𝑦 0 =− 𝑇 𝑈 𝑋 4𝑦0 , wi...

The altitude from𝑀to𝑃𝑁has slope− 𝑥𝑃 −1 𝑦𝑃 and equation𝑦=− 𝑥𝑃 −1 𝑦𝑃 𝑥

Orthocentre𝐻of△𝑃𝑀 𝑁 With𝑀=(0,0),𝑁=(1,0)and𝑃=(𝑥 𝑃, 𝑦𝑃), the altitude from𝑃to𝑀 𝑁is the vertical line𝑥=𝑥 𝑃. The altitude from𝑀to𝑃𝑁has slope− 𝑥𝑃 −1 𝑦𝑃 and equation𝑦=− 𝑥𝑃 −1 𝑦𝑃 𝑥. Intersecting with𝑥=𝑥 𝑃 gives 𝑦= 𝑥𝑃 (1−𝑥 𝑃) 𝑦𝑃 . Hence 𝐻= 𝑥𝑃, 𝑥𝑃 (1−𝑥 𝑃) 𝑦𝑃 . We need the component of𝐻orthogonal to𝐴𝑃, i.e. 𝐻𝑤 =(𝐻−𝐴) ·w. Compute 𝐻−𝐴= 𝑥𝑃 −𝑥 0, 𝑥𝑃 (1−𝑥 𝑃 ) 𝑦𝑃 −𝑦 0 . ...

Hence the circum- centre𝑂has coordinates(𝑆, 𝑘)for some𝑘

Circumcircle of△𝐵𝐸𝐹 The points𝐸, 𝐹lie on the𝑢-axis, so the perpendicular bisector of𝐸𝐹is the line𝑢=𝑆. Hence the circum- centre𝑂has coordinates(𝑆, 𝑘)for some𝑘. Using|𝑂𝐸|=|𝑂𝐵|we obtain 𝑘= (𝑆−𝑏) 2 +ℎ 2 −𝐷 2 2ℎ . Substituting𝑏=𝑈𝑆,ℎ=−2𝑦 0 𝐷, and𝑆−𝑏=𝑆(1−𝑈)=𝑆𝑌 2 (because1−𝑈=𝑌 2) yields (𝑆−𝑏) 2 +ℎ 2 −𝐷 2 =𝑆 2𝑌 4 +4𝑦 2 0 𝐷2 −𝐷 2. We need the expression for4𝑦2

Factorising the numerator as a difference of squares, 4𝑟2 − (1+𝑟 2 −𝑅 2)2 = 2𝑟− (1+𝑟 2 −𝑅 2) 2𝑟+ (1+𝑟 2 −𝑅 2)

Using the coordinates of𝐴, 𝑦2 0 =𝑟 2 −𝑥 2 0 =𝑟 2 − (1+𝑟 2 −𝑅 2)2 4 . Factorising the numerator as a difference of squares, 4𝑟2 − (1+𝑟 2 −𝑅 2)2 = 2𝑟− (1+𝑟 2 −𝑅 2) 2𝑟+ (1+𝑟 2 −𝑅 2) . The first factor equals(𝑅+𝑟−1) (𝑅−𝑟+1)=(𝑋−1) (𝑌+1), the second equals−(𝑌−1)𝑇. Hence 4𝑟2 − (1+𝑟 2 −𝑅 2)2 =𝑇(𝑋−1)𝑈, so that 𝑦2 0 = 𝑇 𝑈(𝑋−1) 4 .(1) Consequently4𝑦 2 0 −1=𝑇 𝑈(𝑋−1) ...

The distance from the centre𝑂=(𝑆, 𝑘)to this line is|𝑘−𝐻 𝑤 |

Tangency condition The line through𝐻parallel to𝐴𝑃is, in the(𝑢, 𝑤)system, the horizontal line𝑤=𝐻 𝑤. The distance from the centre𝑂=(𝑆, 𝑘)to this line is|𝑘−𝐻 𝑤 |. The radius of the circle(𝐵𝐸𝐹)is|𝑂𝐸|= √ 𝐷2 +𝑘 2. Tangency is equivalent to |𝑘−𝐻 𝑤 |= √︁ 𝐷2 +𝑘 2 ⇐ ⇒𝐻 2 𝑤 −2𝑘𝐻 𝑤 =𝐷 2.(2) We now compute each term. 40 MaxProof: Scaling Mathematical Proof with Genera...

2025

- Taking𝑎=𝑏=1gives𝑓(1) |1−𝑓(1) 𝑓(1)

Basic properties Let𝑓:ℕ→ℕbe a bonza function. - Taking𝑎=𝑏=1gives𝑓(1) |1−𝑓(1) 𝑓(1) . Since𝑓(1) |𝑓(1) 𝑓(1) , we have𝑓(1) |1; hence𝑓(1)=1. - Setting𝑏=𝑎yields𝑓(𝑎) |𝑎 𝑎 −𝑓(𝑎) 𝑓(𝑎) . Because𝑓(𝑎) |𝑓(𝑎) 𝑓(𝑎) , it follows that 𝑓(𝑎) |𝑎 𝑎 for every𝑎∈ℕ.(1)

As𝑝 𝑝 is a prime power, 𝑓(𝑝)=𝑝 𝑘 with0≤𝑘≤𝑝

Behaviour on primes For a prime𝑝, (1) implies𝑓(𝑝) |𝑝 𝑝. As𝑝 𝑝 is a prime power, 𝑓(𝑝)=𝑝 𝑘 with0≤𝑘≤𝑝. Define 𝑃={𝑝prime|𝑓(𝑝)>1}

Substituting𝑎=𝑝into the bonza condition gives 𝑝𝑘 |𝑏 𝑝 −𝑓(𝑏) 𝑝𝑘 for all𝑏∈ℕ

Congruence modulo𝑝∈𝑃 Fix𝑝∈𝑃and write𝑓(𝑝)=𝑝 𝑘 with𝑘≥1. Substituting𝑎=𝑝into the bonza condition gives 𝑝𝑘 |𝑏 𝑝 −𝑓(𝑏) 𝑝𝑘 for all𝑏∈ℕ. Work modulo𝑝. By Fermat’s little theorem,𝑥𝑝 ≡𝑥(mod𝑝)for every integer𝑥. An easy induction shows 𝑥 𝑝𝑘 ≡𝑥(mod𝑝) (base𝑘=1is Fermat; if𝑥 𝑝𝑘 ≡𝑥(mod𝑝),then𝑥 𝑝𝑘+1 =(𝑥 𝑝𝑘 ) 𝑝 ≡𝑥 𝑝 ≡𝑥(mod𝑝)). Hence 𝑏𝑝 −𝑓(𝑏) 𝑝𝑘 ≡𝑏−𝑓(𝑏) (mod𝑝), so𝑝|𝑏−𝑓(𝑏)....

Therefore𝑓is the identity function

Structure of𝑃 -If𝑃is infinite, then for each𝑏the number𝑓(𝑏) −𝑏is divisible by infinitely many distinct primes (the primes in𝑃), which forces𝑓(𝑏)=𝑏. Therefore𝑓is the identity function. -Now assume that𝑃is finite and non-empty. We first prove that𝑃cannot contain any odd prime. Suppose, for contradiction, that an odd prime𝑝∈𝑃. By Dirichlet’s theorem, there a...

Fix an arbitrary𝑛∈ℕ

Case analysis Case A:𝑃=∅.Then𝑓(𝑝)=1for every prime𝑝. Fix an arbitrary𝑛∈ℕ. For any prime𝑏we have 𝑓(𝑛) |𝑏 𝑛 −1, because the bonza condition with𝑎=𝑛,𝑏=𝑏gives𝑓(𝑛) |𝑏 𝑛 −𝑓(𝑏) 𝑓(𝑛) =𝑏 𝑛 −1. Hence𝑓(𝑛)divides𝑏 𝑛 −1 foreveryprime𝑏. The greatest common divisor over all primes𝑏of𝑏 𝑛 −1is1: for any prime𝑟we have 𝑟∤𝑟 𝑛 −1. Therefore𝑓(𝑛)=1. Thus𝑓≡1. Case B:𝑃infinite.As...

- If𝑛is even, write𝑛=2 𝑗𝑚with𝑗≥1,𝑚odd; then𝑓(𝑛) ≤2 𝑗+2 ≤4𝑛

Upper bound𝑓(𝑛) ≤4𝑛 Collecting the three cases: - If𝑛is odd,𝑓(𝑛)=1≤4𝑛. - If𝑛is even, write𝑛=2 𝑗𝑚with𝑗≥1,𝑚odd; then𝑓(𝑛) ≤2 𝑗+2 ≤4𝑛. - The identity function also satisfies𝑓(𝑛)=𝑛≤4𝑛. Hencefor every bonza function𝑓and every𝑛∈ℕ, 𝑓(𝑛) ≤4𝑛.(4)

(Equivalently, for even𝑛≠2, write𝑛=2 𝑗𝑚with𝑗≥1,𝑚odd, and set𝑓(𝑛)=2 𝑗+2.) We verify that this𝑓is bonza

Construction achieving the ratio4 Define𝑓by 𝑓(𝑛)=    1,if𝑛is odd, 4,if𝑛=2, 2 𝑗+2,if𝑛=2 𝑗𝑚with𝑗≥1, 𝑚odd, and𝑛≠2. (Equivalently, for even𝑛≠2, write𝑛=2 𝑗𝑚with𝑗≥1,𝑚odd, and set𝑓(𝑛)=2 𝑗+2.) We verify that this𝑓is bonza. Case 1:𝑎odd.Then𝑓(𝑎)=1; the condition holds trivially. Case 2:𝑏odd.Then𝑓(𝑏)=1and we must show𝑓(𝑎) |𝑏 𝑎 −1. - If𝑎is odd,𝑓(𝑎)=1– done...

Therefore the smallest such real constant is 4

Conclusion From (4) we have𝑓(𝑛) ≤4𝑛for every bonza function𝑓and every positive integer𝑛, and the construction above shows that4is the smallest possible constant. Therefore the smallest such real constant is 4 . 45 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling IMO 2025 Problem 4 (Self-Pick: 7/7) Pro...

2025

Thus 𝑒𝑛+1 =𝑒 𝑛 −2, 𝑓 𝑛+1 =𝑓 𝑛 −1, 𝑟 𝑛+1 =13𝑟 𝑛.(1)

The case𝑒𝑛 ≥2.From (*) we have 𝑎𝑛+1 =𝑓(𝑎 𝑛)= 13 12 𝑎𝑛 =13·2 𝑒𝑛 −2 ·3 𝑓𝑛 −1 ·𝑟 𝑛. Thus 𝑒𝑛+1 =𝑒 𝑛 −2, 𝑓 𝑛+1 =𝑓 𝑛 −1, 𝑟 𝑛+1 =13𝑟 𝑛.(1)

47 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling The factor2disappears, and the remaining product is odd

The case𝑒𝑛 =1,5|𝑟 𝑛.Then 𝑎𝑛+1 = 31 30 𝑎𝑛 =31·3 𝑓𝑛 −1 · 𝑟𝑛 5 . 47 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling The factor2disappears, and the remaining product is odd. Hence𝑎𝑛+1 is odd, so6∤𝑎 𝑛+1. By Lemma 1, the sequence would then strictly decrease, contradicting the assumption that it is infinit...

Reaching a fixed point Suppose we start with a term𝑎 1 for which the sequence is infinite

The case𝑒𝑛 =1,5∤𝑟 𝑛.Here𝑓(𝑎 𝑛)=𝑎 𝑛, i.e., the sequence has reached a fixed point. Reaching a fixed point Suppose we start with a term𝑎 1 for which the sequence is infinite. Then we must never enter the forbidden branch𝑒=1,5|𝑟. Consequently, after some number of steps we must arrive at a fixed point with𝑒=1,5∤𝑟. From (1) we see that while𝑒𝑛 ≥2, the exponen...

2025

+𝜆.(2) Since𝜆 > √ 2 2 we have2𝜆− √ 2>0; thus the right-hand side of (2) tends to+∞as𝑘→ ∞. Consequently there exists an integer𝐾such that for all𝑘≥𝐾, 50 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling 𝐴2 2𝑘+1 >(2𝑘+1) +1=2𝑘+2. Hence Alice eventually has a turn with𝐴2 𝑛 > 𝑛+1; on that turn she plays𝑥𝑛 =...

Thus 𝑎≤𝜆 < √ 2 2 < √ 2, so𝑎 2 <2and Bazza’s move𝑏𝑘+1 = √ 2−𝑎 2 is well defined

+𝜆.(4) Because𝜆 < √ 2 2 we have2𝜆− √ 2<0; hence the right-hand side of (4) is decreasing in𝑘and its maximum over𝑘≥0is𝜆. Thus 𝑎≤𝜆 < √ 2 2 < √ 2, so𝑎 2 <2and Bazza’s move𝑏𝑘+1 = √ 2−𝑎 2 is well defined. Then 𝑄2(𝑘+1) =𝑄 2𝑘 +𝑎 2 +𝑏 2 𝑘+1 =2𝑘+𝑎 2 + (2−𝑎 2)=2(𝑘+1). The increase in the sum isΔ𝑆=𝑎+𝑏 𝑘+1. Squaring gives (Δ𝑆) 2 =𝑎 2 +𝑏 2 𝑘+1 +2𝑎𝑏 𝑘+1 =2+2𝑎𝑏 𝑘+1 ≥2, soΔ𝑆≥ √

Now consider Alice’s next turn, number2(𝑘+1) +1=2𝑘+3

Consequently 𝑆2(𝑘+1) =𝑆 2𝑘 +Δ𝑆≥𝑘 √ 2+ √ 2=(𝑘+1) √ 2, completing the induction. Now consider Alice’s next turn, number2(𝑘+1) +1=2𝑘+3. At that moment the sum is𝑆2(𝑘+1) . Using the lower bound𝑆2(𝑘+1) ≥ (𝑘+1) √ 2, it suffices to show 51 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling (𝑘+1) √ 2> 𝜆(2𝑘+3)fo...

Consequently Alice is always forced to choose𝑎≤ √ 2 2

Thus (5) holds for all𝑘. Consequently Alice is always forced to choose𝑎≤ √ 2 2 . Therefore 𝑄2𝑘+1 =𝑄 2𝑘 +𝑎 2 ≤2𝑘+ 1 2 <2𝑘+2=(2𝑘+1) +1, so she never makes𝑄2𝑘+1 >2𝑘+2, which would be necessary to win. Bazza always has a legal move (because𝑎 2 ≤ 1 2 <2) and never loses. Hence Alice has no winning strategy. #### 3B. Bazza cannot force a win Alice plays𝑥 𝑛 =0on...

Conclusion Alice has a winning strategy if and only if𝜆 > √ 2 2 , Bazza has a winning strategy if and only if𝜆 < √ 2 2 , Neither player has a winning strategy if𝜆= √ 2 2 . 53 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling IMO 2025 Problem 6 (Self-Pick: 0/7) Problem Statement Consider a2025×2025grid ...

2025

Let𝑁, the midpoint of the minor arc𝐵𝐶, be(−1,0); the tangent at𝑁is then the line𝑥=−1

Coordinate setupPlace the circumcircle𝜔as the unit circle. Let𝑁, the midpoint of the minor arc𝐵𝐶, be(−1,0); the tangent at𝑁is then the line𝑥=−1. Because𝑁bisects the minor arc𝐵𝐶, the chord𝐵𝐶is vertical. Write 𝐵=(−cos𝜃,−sin𝜃), 𝐶=(−cos𝜃,sin𝜃),0< 𝜃 < 𝜋 2 . The vertex𝐴lies on the major arc𝐵𝐶(the arc not containing𝑁). By reflecting if necessary we may assume𝐴is...

* The equilateral triangleΔ𝐵 has its centre at the origin, so the midpoint of the two vertices different from 𝐵is− 𝐵

Equations of the linesFor a point𝑃on the unit circle the tangent at𝑃has equationX·𝑃=1. * The equilateral triangleΔ𝐵 has its centre at the origin, so the midpoint of the two vertices different from 𝐵is− 𝐵

ℓ𝐵 :𝑥cos𝜃+𝑦sin𝜃= 1 2

The lineℓ𝐵 through those two vertices is parallel to the tangent at𝐵; henceℓ𝐵 :X·𝐵=− 1 2, i.e. ℓ𝐵 :𝑥cos𝜃+𝑦sin𝜃= 1 2 . * Similarly,ℓ𝐶 :𝑥cos𝜃−𝑦sin𝜃= 1 2. * The tangent at𝑁isℓ 𝑁 :𝑥=−1

Line𝐴𝐶meetsℓ 𝐵 at𝑌.Write𝑌=𝐴+𝑢(𝐶−𝐴)

Points𝑌and𝑍Set 𝐶1 =cos(𝛼−𝜃)=cos𝛼cos𝜃+sin𝛼sin𝜃, 𝐶2 =cos(𝛼+𝜃)=cos𝛼cos𝜃−sin𝛼sin𝜃, 𝑄=cos 2𝜃, 𝑀=𝑄+ 1 2 . Line𝐴𝐶meetsℓ 𝐵 at𝑌.Write𝑌=𝐴+𝑢(𝐶−𝐴). Substituting into the equation ofℓ 𝐵 gives 𝐶1 +𝑢(𝑄−𝐶 1)= 1 2 =⇒𝑢= 𝐶1 − 1 2 𝑄+𝐶 1 ,1−𝑢= 𝑀 𝑄+𝐶 1 . Hence 𝑌=(1−𝑢)𝐴+𝑢𝐶. Line𝐴𝐵meetsℓ 𝐶 at𝑍.Analogously, with𝑍=𝐴+𝑣(𝐵−𝐴)we obtain 𝑣= 𝐶2 − 1 2 𝑄+𝐶 2 ,1−𝑣= 𝑀 𝑄+𝐶 2 , and 60 MaxProof...

Because𝐴lies on the unit circle,𝑎 2 +𝑏 2 =1, so 𝐹=−1−𝐷𝑎−𝐸𝑏,where𝑎=cos𝛼, 𝑏=sin𝛼

Circumcircle of△𝐴𝑌 𝑍We look for the circle 𝑥2 +𝑦 2 +𝐷𝑥+𝐸 𝑦+𝐹=0 through𝐴, 𝑌 , 𝑍. Because𝐴lies on the unit circle,𝑎 2 +𝑏 2 =1, so 𝐹=−1−𝐷𝑎−𝐸𝑏,where𝑎=cos𝛼, 𝑏=sin𝛼. Substituting𝑌and𝑍into the circle equation and using𝐹yields the linear system    𝐷(𝑌𝑥 −𝑎) +𝐸(𝑌 𝑦 −𝑏)=1− |𝑌| 2, 𝐷(𝑍 𝑥 −𝑎) +𝐸(𝑍 𝑦 −𝑏)=1− |𝑍| 2. A straightforward computation (using|𝐴|=|𝐵|=|𝐶|=1...

Substituting𝐷, 𝐸 and simplifying yields 𝑂= − 𝑀(1−2 cos𝛼cos𝜃) cos𝛼+cos 3𝜃 , 2𝑀sin𝛼cos𝜃 cos𝛼+cos 3𝜃

Centre and radius of the circumcircleΓof𝐴𝑌 𝑍The centre is𝑂=(−𝐷/2,−𝐸/2). Substituting𝐷, 𝐸 and simplifying yields 𝑂= − 𝑀(1−2 cos𝛼cos𝜃) cos𝛼+cos 3𝜃 , 2𝑀sin𝛼cos𝜃 cos𝛼+cos 3𝜃 . Let 𝐿=cos𝛼+cos 3𝜃, 𝑁=2 cos 2 𝜃−2 cos𝛼cos𝜃+ 1 2 . Using𝑀=2 cos 2 𝜃− 1 2, a direct computation (expanding the squares) shows 𝑂𝐴 2 = 𝑁 2 𝐿2 . Indeed, 61 MaxProof: Scaling Mathematical Proo...

By symmetry its incenter lies on the𝑥-axis

Incircle ofRThe triangleRhas sidesℓ 𝐵,ℓ 𝐶,ℓ 𝑁. By symmetry its incenter lies on the𝑥-axis. Solving the equal-distance condition from a point(𝑥,0)toℓ 𝑁 (𝑥=−1) and toℓ 𝐵 (𝑥cos𝜃+𝑦sin𝜃= 1

gives 𝑥𝐼 =− 1 2(1+cos𝜃) , 𝑟=𝑥 𝐼 +1= 1+2 cos𝜃 2(1+cos𝜃)

Set𝑆=1+cos𝜃

Tangency verificationWe compute𝑂𝐼2. Set𝑆=1+cos𝜃. Then 𝑂𝑥 −𝑥 𝐼 =− 𝑀(1−2𝑎𝑡) 𝐿 + 1 2𝑆 , 𝑂𝑦 = 2𝑀𝑏𝑡 𝐿 . Hence 𝑂𝐼 2 = − 𝑀(1−2𝑎𝑡) 𝐿 + 1 2𝑆 2 + 2𝑀𝑏𝑡 𝐿 2 = 𝑀2(1−2𝑎𝑡) 2 +4𝑏 2𝑡2 𝐿2 − 𝑀(1−2𝑎𝑡) 𝑆𝐿 + 1 4𝑆2 . Using𝑎 2 +𝑏 2 =1, (1−2𝑎𝑡) 2 +4𝑏 2𝑡2 =1−4𝑎𝑡+4𝑡 2. Thus 𝑂𝐼 2 = 𝑀2 (1−4𝑎𝑡+4𝑡 2) 𝐿2 − 𝑀(1−2𝑎𝑡) 𝑆𝐿 + 1 4𝑆2 .(1) Now consider the quantity 𝑅2 +𝑟 2 +2𝑟 𝑁 𝐿 = 𝑁 2 𝐿2 + (1+...

62 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling Verification of (ii): From (i),𝑀2𝑃=2𝑁 𝑀 2, so 𝑀2𝑃−𝑁 2 =𝑁(2𝑀 2 −𝑁)

Since4𝑡 2 =2(2𝑡 2)=2(𝑀+ 1 2 ), we have 𝑃=1−4𝑎𝑡+2𝑀+1=2(𝑀−2𝑎𝑡+1)=2𝑁 . 62 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling Verification of (ii): From (i),𝑀2𝑃=2𝑁 𝑀 2, so 𝑀2𝑃−𝑁 2 =𝑁(2𝑀 2 −𝑁). A direct computation gives2𝑀2 −𝑁=2𝑡𝐿(using𝑀=2𝑡 2 − 1 2 and𝐿=𝑎+4𝑡 3 −3𝑡). Hence (ii) holds. Verification of (iii): S...

2026

Let𝑐𝑖 be the carry into the𝑖-th digit (𝑐0 =0), and let𝑛𝑖 be the𝑖-th digit of𝑛(𝑛0 units)

Addition with carries Consider the addition𝑎+𝑏=𝑛digit by digit, from the units digit upwards. Let𝑐𝑖 be the carry into the𝑖-th digit (𝑐0 =0), and let𝑛𝑖 be the𝑖-th digit of𝑛(𝑛0 units). We must choose𝑎𝑖, 𝑏𝑖 ∈𝐷and a carry𝑐 𝑖+1 ∈ {0,1} such that 𝑎𝑖 +𝑏 𝑖 +𝑐 𝑖 =𝑛 𝑖 +10𝑐 𝑖+1. The left-hand side can be any integer between0and18except1, because the set of sums of t...

*𝑐 𝑖 =0:then𝑥=𝑛 𝑖 +10𝑐 𝑖+1

Possible transitions of the carry We examine the two possible values of𝑐𝑖. *𝑐 𝑖 =0:then𝑥=𝑛 𝑖 +10𝑐 𝑖+1. –𝑐𝑖+1 =0possible iff𝑛 𝑖 ≠1. –𝑐𝑖+1 =1possible iff𝑛 𝑖 ≤8. *𝑐 𝑖 =1:then𝑥=𝑛 𝑖 +10𝑐 𝑖+1 −1. –𝑐𝑖+1 =0possible iff𝑛 𝑖 ∈ {1,3,4,5,6,7,8,9}(i.e.𝑛 𝑖 ≥1and𝑛 𝑖 ≠2). – 𝑐𝑖+1 =1is always possible. This can be viewed as a nondeterministic finite automaton (NFA) with sta...

The transitions are: *From𝐴:1↦→𝐵,9↦→𝐴,all other digits↦→𝐶

From the NFA to a DFA The NFA has only two states, so the subset construction yields a DFA with states𝐴={0}, 𝐵={1}, 𝐶= {0,1}. The transitions are: *From𝐴:1↦→𝐵,9↦→𝐴,all other digits↦→𝐶. 64 MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling *From𝐵:0,2↦→𝐵,all other digits↦→𝐶. *From𝐶:every digit↦→𝐶(absorbing)

The accepting states are those containing0, i.e.𝐴and𝐶

When is a number solitary? A number𝑛(written with𝐿digits) is accepted by the DFA iff it can be expressed as a sum of two1-free numbers. The accepting states are those containing0, i.e.𝐴and𝐶. Therefore𝑛isnotsolitary (i.e. it belongs to𝐴+𝐴) iff the DFA computation ends in𝐴or𝐶; it is solitary iff the computation ends in𝐵. To end in𝐵the computation must never...

Hencethenumberofsolitarynumberswiththe1atposition𝑡is2 𝐿−𝑡−1

Counting the solitary numbers For a fixed𝑡we have: * the𝑡trailing digits are forced to be9(one way); * the digit at position𝑡is1(one way); * the remaining 𝐿−𝑡−1higher digits can be chosen independently as0or2(2 𝐿−𝑡−1 possibilities). Hencethenumberofsolitarynumberswiththe1atposition𝑡is2 𝐿−𝑡−1. Summingoverall𝑡=0,1, . . . , 𝐿−1 gives 𝐿−1∑︁ 𝑡=0 2𝐿−𝑡−1 = 𝐿−1∑︁...

2026