PROVED (LEAN): the site labels the problem PROVED (LEAN). The first question was answered yes by Danzer at the 1985 Siófok meeting, as Erdős reports, and the second by Boris Alexeev in the site's comments (January 2026) with the unit square as the region; see the claim pages of Danzer and Alexeev. Erdős's paper gives a second finite example for the first question, its Figure 4, found by a participant of the meeting whom he does not name; it has no claim page of its own because its claimant is unnamed. Alexeev's repository holds Lean proofs of both questions: the proof of the second is his own construction formalized, linked on his page, and the proof of the first formalizes the Figure 4 example and is recorded as an independent claim on its own page.