IMO 2025 P1

Stream: IMO-grand-challenge

[Jakob von Raumer]

Has anyone tried manually formalizing P1? Especially in a way that first captures only colinearity and then shows that the given subset of $\mathbb{R}^2$ models this relation?

[Jakob von Raumer]

(Configuration.HasLines ?)

[Jason Rute]

@Jakob von Raumer you mean a solution to P1?

[Jakob von Raumer]

Uh, yes

[Floris van Doorn]

No, but I did do ~half of P3: https://github.com/leanprover-community/mathlib4/compare/master...imo2025-3
This took me about 2.5 hours, already starting from a non-formalized solution. (This is a much worse problem statement than given by Joseph Myers.)

[Bolton Bailey]

Jakob von Raumer said:

Has anyone tried manually formalizing P1? Especially in a way that first captures only colinearity and then shows that the given subset of $\mathbb{R}^2$ models this relation?

I have been working on a solution for Numina over the past week, but it's been a bit of a slog, I am about 400 lines in, but most of the finicky-seeming edges cases aren't done yet. :oh_no: I haven't tried anything particularly complicated in terms of modelling collinearity relationships precisely.

[Jakob von Raumer]

@Bolton Bailey Uploaded the start of my attempt here. I think it would be nice to have a full proof of this in the archive as a benchmark for this kind of geometric combinatorics problem. Not sure when I'll find the time to continue on this. Showing that $k=2$ is impossible for $n = 3$ is already not that easy.

[Notification Bot]

6 messages were moved here from #IMO-grand-challenge > IMO 2025 problem statements by Jason Rute.

[Jason Rute]

This is not human formalized, but the seed prover AI proof for P1 has been posted here if it helps: https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p1.lean

[Jakob von Raumer]

Yes, I saw that it actually manages to exclude the $k = 2$ case

[Jakob von Raumer]

Jason Rute said:

This is not human formalized, but the seed prover AI proof for P1 has been posted here if it helps: https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p1.lean

Did the AI come up with the formalization of the problem statement here? Distinguishing between functions and verticals might actually be the best choice here.

[Zheng Yuan]

Jakob von Raumer said:

Jason Rute said:

This is not human formalized, but the seed prover AI proof for P1 has been posted here if it helps: https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p1.lean

Did the AI come up with the formalization of the problem statement here? Distinguishing between functions and verticals might actually be the best choice here.

human formalized problem statement, AI prove it

[Jakob von Raumer]

@Joseph Myers Do you think it's good to have lemmas like this one in mathlib? (Maybe generalized to points instead of !₂[x₀, y₀])

lemma mem_line_iff {p} {x₀ x₁ y₀ y₁ : ℝ} (hx : x₀ ≠ x₁ ∨ y₀ ≠ y₁ := by grind) :
    p ∈ line[ℝ, !₂[x₀, y₀], !₂[x₁, y₁]] ↔ (p 0 - x₀) * (y₁ - y₀) = (p 1 - y₀) * (x₁ - x₀) := by
  sorry

They make my life much easier solving this problem and I couldn't find anything like this in mathlib. Same for equalities of lines, colinearity of points, ...

[Joseph Myers]

There have been comments before about the difficulty in applying abstract mathlib geometry to concrete expressions with coordinates. I think it's reasonable to add such lemmas for use in applications (probably not going to be used much in mathlib itself since mathlib lemmas are generally for an arbitrary affine space). The above statement should work for any Fin 2 → 𝕜 for a field 𝕜 (using ![...] in that case, of course), with the EuclideanSpace / !₂[...] lemma then being a variant for that specific case (the two statements should be defeq, but users should avoid abusing that defeq, so both statements should be provided).

[Joseph Myers]

A previous discussion concerned computing angles with a concrete orientation of EuclideanSpace, and I think that definitely showed up missing lemmas as well.

[Joseph Myers]

There may be scope for slightly more abstract versions of the lemmas where you're given a Fin 2 basis of a space rather than making it literally one of the two concrete spaces referred to above, but the versions with Fin 2 → 𝕜 and EuclideanSpace make sense as well.

[Jakob von Raumer]

Thank you for your comments! Will see when I find the time to complete the formalization of the solution, will PR the helper lemmas then

[Jakob von Raumer]

Created a WIP PR at #27813 for this. Happy to receive feedback, there's a few geometric sorries and one combinatoric sorry left. I mostly stuck to the problem statement given by @Joseph Myers

[Jakob von Raumer]

Will move some of the preliminaries to their own PRs once it's fleshed out

[Yizheng Zhu]

Hi I am a new contributor and I have made a PR with the solution:
https://github.com/leanprover-community/mathlib4/pull/27817
It would be best to have an API for hyperplanes in n-dimensional vector spaces, dimensions of hyperplanes, (hyper)-colinarity, etc., in mathlib, and use that API. If necessary, I will be happy to contribute to the relevant parts of mathlib.

[Jakob von Raumer]

Let's first pull out all the preliminaries about the plane then, your file seems more complete than mine in that aspect! Then we can afterwards see how we can patch together the most succint proof of the problem from our files :smiley:

[Joseph Myers]

Both PRs have lemmas such as

lemma point_sub {x₁ y₁ x₂ y₂ : ℝ} : !₂[x₁, y₁] - !₂[x₂, y₂] = !₂[x₁ - x₂, y₁ - y₂] := by
  ext i; fin_cases i <;> simp

or

lemma vec_mul (k x y : ℝ) : k • !₂[x, y] = !₂[k * x, k * y] := by
  ext i; fin_cases i <;> simp

that are meaningful for vectors with explicit coordinates in any number of dimensions, not just two dimensions. Maybe that means they should actually be implemented as simprocs (and also implemented to work with other subscripts, not just 2, i.e. for WithLp.toLp in general, though other subscripts would probably be rarely used).

(Note: I've never written a simproc, but there's a guide to them on the community blog. There may also be other approaches not involving simprocs to allow such lemmas to apply for any number of coordinates.)

[Eric Wieser]

I have a PR open that works towards these; in the meantime both statements can be proved with FinVec.etaExpand_eq _ |>.symm

[Eric Wieser]

I think it might be preferable to use what I'm calling a "rw_proc", which eschews the simp machinery in favor of abusing autoParams, and works in rw as a result