Certified values of reciprocal Rado numbers, and a minimum over unit fractions

Abstract

For k ≥ 2 and r ≥ 1 the reciprocal Rado number fᵣ(k) is the least n such that every r-colouring of {1,…,n} admits a monochromatic solution of 1/x₁+…+1/xₖ=1/xₖ₊₁, the xᵢ not necessarily distinct. Gaiser and Ramezanpour recently proved the sharp bound f₂(k) ≥ 3k² for k ≥ 3, tabulated 28 values of fᵣ(k), twenty-four of them computed there for the first time by SAT solving, and posed four problems. We contribute two things. First, a decision procedure for fᵣ(k) in which every step is machine-checked: a backtracking enumeration of the solution set of the equation, proved both complete and sound; a conjunctive normal form encoding whose fidelity — every avoiding colouring satisfies the formula — is proved rather than asserted; and refutations replayed inside a proof assistant from LRAT certificates. It delivers f₂(2)=60, f₂(3)=40, f₂(4)=48, f₂(5)=80, f₃(3)=585 and f₃(2)=3276 as two-sided theorems carrying certificates, and we are aware of no earlier machine-checkable certificate for a reciprocal Rado number. Second, we determine the first twenty-five values of the quantity of Problem 5.4 of Gaiser and Ramezanpour: the least positive value of a-b₁-…-bₖ with a,b₁,…,bₖ unit fractions of denominator at most n. The answer is not always a unit fraction — at k=2, n=16 it is 5/1456 — so the shape of the k=1 case does not persist, and it is not monotone in k. Every theorem below is formally verified in Lean 4.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-08-30 15:34 UTC

   File fingerprint

   9ae466a447ab69c09050940a274c70254aead69866339c2352cc365bd14a3ceb