combinatorics in mathlib

Stream: general

[Ilia Zgonnik]

Newbie here.

Guys, can someone send me info why Lean is still bad at combinatorics? Which for people easy steps are not available to lean. Is problem more about lack of combinatorics theorems in mathlib or something else?

[Notification Bot]

A message was moved here from #general > new monadic program verification framework by Ruben Van de Velde.

[Yaël Dillies]

Hey :wave: Can you clarify what you mean by "bad at combinatorics"? It's bad at combinatorics in the sense that it doesn't have much of it, but it's good at combinatorics in the sense that it's relatively easy to do any simple combinatorics on top of it. It also heavily depends on what subfield of combinatorics you're thinking about.

[Ilia Zgonnik]

Yaël Dillies said:

Hey :wave: Can you clarify what you mean by "bad at combinatorics"? It's bad at combinatorics in the sense that it doesn't have much of it, but it's good at combinatorics in the sense that it's relatively easy to do any simple combinatorics on top of it. It also heavily depends on what subfield of combinatorics you're thinking about.

For some problems it is very hard to write even a problem (not speaking of solution) in Lean. It struggles a lot with hard problems with cells. I just think there are a lot of techniques in combinatorics which you can’t write in Lean

[Ilia Zgonnik]

Ilia Zgonnik said:

Yaël Dillies said:

Hey :wave: Can you clarify what you mean by "bad at combinatorics"? It's bad at combinatorics in the sense that it doesn't have much of it, but it's good at combinatorics in the sense that it's relatively easy to do any simple combinatorics on top of it. It also heavily depends on what subfield of combinatorics you're thinking about.

For some problems it is very hard to write even a problem (not speaking of solution) in Lean. It struggles a lot with hard problems with cells. I just think there are a lot of techniques in combinatorics which you can’t write in Lean

For example, can we write combinatorics with number greater than 3 in IMO shortlist in Lean? Can AI do it? I think there are so many good solutions in Lean for hard combinatorics, that AI can’t train normally. And creating such dataset is very hard task to do, because it requires really good mathematicians and Lean pros :)

[Joseph Myers]

Ilia Zgonnik said:

For example, can we write combinatorics with number greater than 3 in IMO shortlist in Lean?

I wrote formal solutions to both combinatorics problems from IMO 2024, which were C4 and C7, so yes.

[Ilia Zgonnik]

Joseph Myers said:

Ilia Zgonnik said:

For example, can we write combinatorics with number greater than 3 in IMO shortlist in Lean?

I wrote formal solutions to both combinatorics problems from IMO 2024, which were C4 and C7, so yes.

Can you send link to them, please

[Joseph Myers]

https://github.com/leanprover-community/mathlib4/blob/master/Archive/Imo/Imo2024Q3.lean
https://github.com/leanprover-community/mathlib4/blob/master/Archive/Imo/Imo2024Q5.lean

[Jeremy Tan]

I have also written some solutions to combinatorics problems that are in the Archive folder of mathlib

[Kim Morrison]

I suspect this question is based on a misunderstanding: the AIs trying to do IMO level combinatorics problems in Lean are not very good at that task. I suspect the OP may have conflated this idea with the idea that it is hard to do combinatorics in Lean. This does not follow. :-)

[Joseph Myers]

It does seem there is a greater distance between an informal solution and a corresponding formal solution for such problems, compared to algebra or number theory problems. This might mean that AIs that produce an informal solution then formalize it have an advantage on such problems compared to AIs that search directly for a Lean proof, or might mean that there are general lemmas and tactics we're missing that could improve the experience of writing such proofs in Lean. (It would be interesting if an AI could mine large amounts of Lean proofs to look for common patterns that should be converted into lemmas or tactics.)

[Ilia Zgonnik]

Kim Morrison said:

I suspect this question is based on a misunderstanding: the AIs trying to do IMO level combinatorics problems in Lean are not very good at that task. I suspect the OP may have conflated this idea with the idea that it is hard to do combinatorics in Lean. This does not follow. :-)

I thought that if people can write proof in lean for combinatorics, then AI can also. What’s the problem for AI to get good at formalizing combinatorics in lean? Because it already produces great natural language proofs, able to break problem in lemmas, but when it comes to checking itself, it crushes.

[Kim Morrison]

Ilia Zgonnik said:

I thought that if people can write proof in lean for combinatorics, then AI can also.

This is still far from the truth. :-)

[Ilia Zgonnik]

Kim Morrison said:

Ilia Zgonnik said:

I thought that if people can write proof in lean for combinatorics, then AI can also.

This is still far from the truth. :-)

Is problem with dataset? Because it seems like routine work in which AI is good at