{"id":"palomar/PALOMAR-2026-10-11-000015","url":"https://github.com/raphaeldelors-code/palomar-erdos607/tree/45ef2462f0a9f139734ac590238456229bca068b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000015-v1.json","repo":"https://github.com/raphaeldelors-code/palomar-erdos607","tags":["math.CO","msc:05D10","msc:52C10","combinatorial-geometry","pbd","lean-formalization"],"score":0,"title":"Erdos607","trust":"high","domain":"math.CO","source":"palomar","authors":["Raphael Delors"],"reviews":0,"subject":"math.CO","summary":"Machine-checked upper bound on Erdős problem 607. For n ≥ 2 let F(n) be the number of distinct multiplicity sets A(P) that can arise from a collection P of n points of the plane, where A(P) is the set of block sizes (point counts) of the lines determined by P. The proof shows that the lines of P form a pairwise-balanced design on the n points (every pair of points lies on exactly one line, and each line contains at least two points), so A(P) is exactly the set of block sizes of such a PBD. Hence F(n) is bounded by the number of PBD profile sets on n points, and the Colbourn–Phelps–Rödl…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true}