Aharoni–Korman conjecture formally disproved

Stream: mathlib4

[Bhavik Mehta]

The Aharoni–Korman conjecture (also known as the fishbone conjecture) was disproved near the end of 2024 by Lawrence Hollom. I formalised this disproof, which is now available as its own repo: https://github.com/b-mehta/AharoniKorman, or in #20082.

The conjecture stood for around 30 years, and has been described as central in its field. Some more information about the conjecture is here:

• https://x.com/wtgowers/status/1862811821083681257
• https://www.youtube.com/watch?v=YQnEB5rio_A
  

I'd like to PR this to mathlib, especially because the statement can be easily written without adding any new defs to mathlib:

theorem aharoni_korman_false :
    ¬ ∀ (α : Type) (_ : PartialOrder α),
        (∃ A : Set α, IsAntichain (· ≤ ·) A ∧ A.Infinite) ∨
        (∃ C : Set α, IsChain (· ≤ ·) C ∧
         ∃ S : Set (Set α), Setoid.IsPartition S ∧
          ∀ A ∈ S, IsAntichain (· ≤ ·) A ∧ (A ∩ C).Nonempty) := by

Excluding the generic lemmas (which are now all in their own mathlib PRs), the disproof amounts to about 1000 lines of code, including some comments.

Along the way, it turned out the proof required quite a few substantial changes, which Lawrence was very helpful with. This is yet another example of maths being formalised "in real-time", partially because the Lean 4 proof was sorry-free a little over a month after it was made public, and because large parts of the final proof were only found after formalisation was started.

I originally PRed this toMathlib/Counterexamples (in #20082), since the disproof is fairly long and (to the best of my knowledge) the intermediate definitions and theory isn't useful for much else. Do people generally agree this should be in Mathlib/Counterexamples?
If so, should it be split up into a sequence of small PRs, all to the same file? To me, this seems harder to review since the context for the theory would be completely absent.

[Bhavik Mehta]

Oh, as an aside, the omega tactic was super useful here: I use it 71 times throughout the proof, excluding the times where aesop used it (which I'd guess is about 10)

[Kim Morrison]

I think a single PR is best here.

[Bhavik Mehta]

The preprint has since been updated to mention the Lean version, and to fix the gaps that were found in the proof. Unfortunately while that removed a couple of errors in the preprint, it introduced two more!
image.png
Namely, I didn't show that the poset is countable and scattered, and that the code isn't yet in mathlib! I rushed to add proofs of countable and scattered to the PR (along with a bunch more documentation and explanation).

[Bhavik Mehta]

If you'd like to help fix the second one, there's only two more remaining PRs: #20756 and #20082.

[Johan Commelin]

Smart way to make sure your PRs will be merged quickly /jk :rofl:

[Johan Commelin]

@Yaël Dillies how is your investigation on #20756 going?

[Bhavik Mehta]

Johan Commelin said:

Smart way to make sure your PRs will be merged quickly /jk :rofl:

I should do it more often :rolling_on_the_floor_laughing:

[Yaël Dillies]

Johan Commelin said:

Yaël Dillies how is your investigation on #20756 going?

Drowning in my notification inbox, but I'll eventually get to it