{"id":"palomar/PALOMAR-2026-10-11-000014","url":"https://github.com/yuhangshi888/erdos-206-explicit-counterexample/tree/b0c255255c1b8ba45fd0ab6c693ecce747fd602f/formalization","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000014-v1.json","repo":"https://github.com/yuhangshi888/erdos-206-explicit-counterexample","tags":["math.NT","math.LO","msc:11D68","msc:03D78","number-theory","transcendental-numbers","lean-formalization"],"score":0,"title":"An explicit computable transcendental counterexample for Erdős Problem #206","trust":"high","domain":"math.NT","source":"palomar","authors":["Yuhang Shi"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of a deterministic rational nested-interval construction defining a particular transcendental real x in (1/4,1/3). For this x, no strictly increasing infinite sequence of positive integer denominators is optimal among all distinct-denominator strict Egyptian underapproximations at every order from any finite starting order onward. The formalization includes the fully specified terminating construction, all prefix and polynomial enumerations, a total executable rational approximation function, and the error bound |x-q_n| = 0. It also proves attainment of the best finite…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"A computable transcendental number without eventually greedy best Egyptian underapproximations","identifier":"doi:10.5281/zenodo.23283007","relationship":"formalizes"},{"title":"On eventually greedy best underapproximations by Egyptian fractions","identifier":"arXiv:2406.07218v3","relationship":"adapts"}]}