Using Lean for combinatorics class

Stream: general

[racecar]

Hello, I'm doing a course on combinatorics and I'm bad at structuring and thinking in proofs. I looked around for an iterative / hacker approach to mathematics and I found Lean. Can I use Lean to quickly iterate on problems and figure out if my solutions are correct without going to the professors to ask for help? I've installed everything, it works great, and now I'm trying to encode a problem that I want to solve through double counting. I'm proving an identity. Is this possible in Lean?

[Bryan Gin-ge Chen]

It's certainly possible, but it could be a lot of work depending on what you're trying to prove (potentially more than just going to ask your professor).

[Bhavik Mehta]

It's definitely possible to do double-counting proofs in Lean, though it's not very convenient to do yet

[Oliver Nash]

I formalised a double counting argument here: https://github.com/leanprover-community/mathlib/blob/master/archive/imo/imo1998_q2.lean

[Oliver Nash]

It was quite a bit of work but not as hard as I had feared