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