feat : add complete formal solution for IMO 2025 P6

[lean-tom]

Summary

I have successfully formalized the complete solution for IMO 2025 Problem 6 . To my knowledge, this is the first complete formalization of this problem in Lean 4 without any sorry.

The proof consists of approximately 4,700 lines and is fully compatible with Lean v4.28.0-rc1 and the latest Mathlib.

Methodology

The solution utilizes a multi-disciplinary approach to handle the complexity of the grid configuration:

1. Lower Bound (Necessity - Topological Combinatorics)

We establish the lower bound $n + 2\sqrt{n} - 3$ by applying the Erdős–Szekeres Theorem to the coordinates of the uncovered (black) squares.

• Set-Theoretic Topological Partitioning: Instead of using step functions or explicit analytic boundary lines, the regions are defined through unions and intersections of discrete set intervals. This avoids the complexity of manual max/min casework at the boundaries where LIS and LDS relations shift.
• Topological Pivot in the Disjoint Case: In cases where the LIS and LDS do not intersect, a "topological pivot" is defined as a specific region of white squares. This allows us to identify the pivot's properties without needing to compute an explicit analytic intersection point.
• Precise Counting Strategy: To achieve the exact count of $k^2+2k−3$ tiles, we developed a counting method based on the base black squares rather than the white squares themselves.
  Boundary Filtering: We handled the grid boundary conditions by filtering the set of black squares (using $0<x<k^2−1$, $0<y<k^2−1$). This allowed us to systematically remove the 4 "out-of-bounds" labels that would otherwise extend beyond the grid, ensuring the formal count matches the required upper bound without grueling manual casework on the edges.
• Erdős–Szekeres Theorem: Applied to the coordinates to extract the Longest Increasing Subsequence (LIS) and Longest Decreasing Subsequence (LDS). The theorem guarantees that the product of their lengths is at least $n$, establishing the fundamental bound.

2. Upper Bound (Sufficiency - Elementary Number Theory)

For $n=k^2$ (specifically $n=2025$), we provide an explicit construction:

• Index-Based Fiber Construction: To ensure disjointness, we define two integer forms for each point $p = (x, y)$:

  • $val_s(p) = x + ky + k + 1$
  • $val_t(p) = kx - y + k^2 + k$

• Fiber Mapping: We consider the fibers of the mapping $p \mapsto (s, t)$, where:

  • $s = \lfloor val_s(p) / (k^2 + 1) \rfloor$
  • $t = \lfloor val_t(p) / (k^2 + 1) \rfloor$
    This integer division (Gaussian bracket) naturally partitions the grid into disjoint regions.

• Lattice-Point Black Squares: The uncovered (black) squares are precisely the "lattice points" where both forms are divisible by $k^2 + 1$:

  all_black = { $p$ | $val_s(p) \equiv 0 \pmod {k^2 + 1}$ and $val_t(p) \equiv 0 \pmod {k^2 + 1}$ }

  The Matilda tiles are then defined by removing the black squares from these fibers:
  M_(s, t) = { $p$ | $s = \lfloor val_s(p) / (k^2 + 1) \rfloor$ and $t = \lfloor val_t(p) / (k^2 + 1) \rfloor$ } \ all_black

• Disjointness and Geometry:

  • By Construction: Since the fibers partition the grid, the tiles are guaranteed to be disjoint.
  • Geometric Proof: Using elementary number theory, we formally prove that each such tile corresponds to a $k \times k$ square (clipped at the grid boundaries) that sits to the immediate right of a black square.
  • Verification: We formally verify that this results in exactly $k^2 + 2k - 3$ tiles, covering all white squares.

Acknowledgments & Attribution

Division of Labor

Lead Architect (human): Conceived the global proof strategy and decomposed the problem into a granular series of verifiable lemmas. Key strategic contributions include the set-theoretic topological partitioning, the fiber-based linear congruence system, and the boundary-filtering logic.

AI Assistant (Gemini 3 Pro): Provided implementation support, translating human-designed lemmas into Lean 4 syntax and assisting with the iterative refinement of local proof steps.

Methodology
This formalization is the result of a human-led, iterative process. While AI was used to accelerate implementation, the logical architecture and lemma decomposition were entirely human-driven. Every strategic leap was a conscious mathematical decision, ensuring that the final proof reflects a genuine conceptual understanding of the problem.

[dwrensha]

Please move the new file into the directory Compfiles/, where the rest of the problem files live.

[dwrensha]

When I open this file in my code editor I see many errors.

[dwrensha]

Thank you for fixing the errors. There are still many warnings like

Messages below:                                                                                                                                                                                           
81:0:                                                                                                                                                                                                     
automatically included section variable(s) unused in theorem `Imo2025P6.mem_rect`:                                                                                                                        
  [NeZero n]                                                                                                                                                                                              
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:                                                                                       
  omit [NeZero n] in theorem ...                                                                                                                                                                          
                                                                                                                                                                                                          
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`                                                                                                                        
102:0:                                                                                                                                                                                                    
automatically included section variable(s) unused in theorem `Imo2025P6.eq_of_px_eq`:                                                                                                                     
  [NeZero n]                                                                                                                                                                                              
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:                                                                                       
  omit [NeZero n] in theorem ...                                                                                                                                                                          
                                                                                                                                                                                                          
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`                                                                                                                        
107:0:                                                                                                                                                                                                    
automatically included section variable(s) unused in theorem `Imo2025P6.eq_of_py_eq`:                                                                                                                     
  [NeZero n]                                                                                                                                                                                              
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:                                                                                       
  omit [NeZero n] in theorem ...                                                                                                                                                                          
                                                                                                                                                                                                          
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`                                                                                                                        
120:0:                                                                                                                                                                                                    
automatically included section variable(s) unused in theorem `Imo2025P6.chain_u_mono_le`:                                                                                                                 
  [NeZero n]                                                                                                                                                                                              
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:                                                                                       
  omit [NeZero n] in theorem ...                              

Please fix them too.

[lean-tom]

Hi @dwrensha!
Linter warnings fixed, sections reorganized, and the collaborative process documented. The build is now clean and ready for review!

[dwrensha]

Thanks! Squashed and merged in 435d0fe.