Zulip Chat Archive

Stream: general

Topic: Using Lean for combinatorics class

view this post on Zulip racecar (Nov 12 2020 at 17:48):

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?

view this post on Zulip Bryan Gin-ge Chen (Nov 12 2020 at 17:54):

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).

view this post on Zulip Bhavik Mehta (Nov 12 2020 at 17:58):

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

view this post on Zulip Oliver Nash (Nov 12 2020 at 18:46):

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

view this post on Zulip Oliver Nash (Nov 12 2020 at 18:47):

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

Last updated: May 11 2021 at 13:22 UTC