I had some fun with this. I was pretty proud of myself that I managed to get a 17 step proof (18, including the final refl) of (a+b)^2 = a^2 + b^2 + 2*a*b, without resorting to the simp or repeat tactics. [0] That seems to be the current known record, and I doubt it can be much shorter.
If you restrict yourself to not using simp, it feels a lot like programming in a macro assembly language, IMO. I'd like to try this for something more closely resembling real work sometime, except that I'd use some of the higher level tactics to make it less like assembler and more like Prolog or SQL.
FYI, there are git repos of solutions out there, but, IMO, you get a lot more out of it by doing the proofs yourself. My initial proof of (a+b)^2 = a^2 + b^2 + 2 * a * b was something like 27 statements long. Shortening it to 17 was a fun challenge I'd hate to have cheated myself out of. But, then, I'm the kind of dog who literally would spend hours simplifying a proof for a linear algebra exercise in grad school down from a full paragraph to 2 lines. :P
---
[0]: In fact, the proof is literally just 17 simple rw statements, followed by refl. Using rw ← $THEOREM to get rid of parenthesis was a key tactic, as was using $two_eq_succ_one* to get numbers you can deal with using previous theorems.
I had some fun with this. I was pretty proud of myself that I managed to get a 17 step proof (18, including the final refl) of (a+b)^2 = a^2 + b^2 + 2*a*b, without resorting to the simp or repeat tactics. [0] That seems to be the current known record, and I doubt it can be much shorter.
If you restrict yourself to not using simp, it feels a lot like programming in a macro assembly language, IMO. I'd like to try this for something more closely resembling real work sometime, except that I'd use some of the higher level tactics to make it less like assembler and more like Prolog or SQL.
FYI, there are git repos of solutions out there, but, IMO, you get a lot more out of it by doing the proofs yourself. My initial proof of (a+b)^2 = a^2 + b^2 + 2 * a * b was something like 27 statements long. Shortening it to 17 was a fun challenge I'd hate to have cheated myself out of. But, then, I'm the kind of dog who literally would spend hours simplifying a proof for a linear algebra exercise in grad school down from a full paragraph to 2 lines. :P
---
[0]: In fact, the proof is literally just 17 simple rw statements, followed by refl. Using rw ← $THEOREM to get rid of parenthesis was a key tactic, as was using $two_eq_succ_one* to get numbers you can deal with using previous theorems.
Prior discuussion 1 year ago: https://news.ycombinator.com/item?id=22801607