Status
On this page
Status
Topics
Status
On this page
Status
Topics
Let be a bipartite graph on vertices such that one part has vertices. Is there a constant such that if has at least edges then must contain a ?
Source: erdosproblems.com/1080
An accepted solution exists. The statement is false.
Disproved. The site's label is DISPROVED (LEAN), whose catalog suffix is explained under Formalization; the original texts are not held. The site's commentary credits the negative answer to de Caen and Székely [DeSz92]; their bounds are for and for (the general bound the site also attributes to Faudree and Simonovits), and the commentary records that Lazebnik, Ustimenko and Woldar [LUW94] later raised the lower bound to . A - and -free bipartite graph with parts of sizes about and and edges, fixed, has more than edges for every once is large, so no constant exists and the answer is no. Two claim pages record these results as accepted, on the site's acceptance and, for [LUW94], its refereed publication: de Caen and Székely and Lazebnik, Ustimenko and Woldar. Every exponent is second-hand: [DeSz92], a chapter of a 1992 Bolyai Society volume, and [LUW94], a journal paper whose Crossref record lists the publisher's open-archive license, are not held (the routes tried are recorded below). The external Lean file behind the site's suffix, which declares itself a formalization of de Caen and Székely's solution and is linked from their claim page (De Caen and Székely, 1992), proves, in its own statement, that for every some bipartite graph on vertices with a part of exactly vertices and at least edges has no -cycle, by the Lazebnik--Ustimenko--Woldar construction; it has not been built here. The standing derives from the two accepted claim pages, on the curator's credit for [DeSz92] and on the journal publication of [LUW94]; the Lean file is a formalization link, not evidence; and the exponents stay second-hand until [DeSz92] or [LUW94] is read at its theorem.