48

18 Steps (-a)*(-a) = ((-a)*(-a))+0 Axiom 2 = ((-a)*(-a))+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a))))) Axiom 3 = (((-a)*(-a))+((a*a)+(a*(-a))))+(-((a*a)+(a*(-a)))) Axiom 1 = (((a*a)+(a*(-a)))+((-a)*(-a)))+(-((a*a)+(a*(-a)))) Axiom 4 = ((a*a)+((a*(-a))+((-a)*(-a)...


29

18 steps Different from the already posted 18-step solution. a*a = a*a + 0 A2 = a*a + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a)))) A3 = (a*a + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a))) A1 = (a*a + a*((-a) + (-a))) + (-(a*(-a) + a*(-a))) A8 = a*(a + ((-a) + (-a))) + (-(a*(-...


28

29 26 Steps No lemmas! Comment if you see anything wrong. (It's very easy to make a mistake) (-a) × (-a) = ((-a) + 0) × (-a) Ax. 2 = ((-a) + (a + (-a))) × (-a) Ax. 3 = ((a + (-a)) + (-a)) × (-a) Ax. 4 ...


25

88 82 77 72 steps Thanks to H.PWiz for better combinator conversions that saved 10 steps! Explanation You might be familiar with the Curry–Howard correspondence, in which theorems correspond to types and proofs correspond to programs of those types. The first two axioms in the Łukasiewicz system are actually the K and S combinators, and it’s well known ...


24

91 Steps Full Proof: 1. (A → B) → (¬¬A → (A → B)) LS1 2. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)) LS2 3. ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) → ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) LS1 4. (A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) MP 3,2 5. ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) → (((A → B) → (¬¬A → (A ...


15

18 steps Not the first 18-step proof, but it’s simpler than the others. (-a)*(-a) = (-a)*(-a) + 0 [Axiom 2] = (-a)*(-a) + ((-a)*a + -((-a)*a)) [Axiom 3] = ((-a)*(-a) + (-a)*a) + -((-a)*a) [Axiom 1] = ((-a)*(-a) + ((-a) + 0)*a) + -((-a)*a) [Axiom 2] = ((-a)*(-a) + ((-a)*a + 0*a)) + -((-a)*a) [Axiom 9] = (((-...


14

59 steps Norman Megill, author of Metamath has told me about a 59 step proof, which I'm going to post here in this community wiki. The original can be found in theorem 2.16 on this page. http://us.metamath.org/mmsolitaire/pmproofs.txt Norm says: This page would provide plenty of challenges for you to beat! Here's the proof ((P -> Q) -> (~ Q -> ...


9

A2: (-a) x (-a) = ((-a) + 0) x (-a) A3: = ((-a) + (a + (-a))) x (-a) A9: = ((-a) x (-a)) + ((a + (-a)) x (-a)) A4: = ((-a) x (-a)) + (((-a) + a) x (-a)) A9: = ((-a) x (-a)) + (((-a) x (-a)) + (a x (-a))) A1: = (((-a) x (-a)) + ((-a) x (-a))) + (a x (-a)) A2: = (((-a) x (-a)) + ((-a) x (-...


7

19 steps (()) [double cut] (AB()(((G)))) [insertion] (AB(A)(((G)))) [iteration] (((AB(A)))(((G)))) [double cut] (((AB(A))(((G))))(((G)))) [iteration] (((AB(A))(((G))))((H(G)))) [insertion] (((AB(A))(((G)(()))))((H(G)))) [double cut] (((AB(A))(((DE()(C)(F))(G))))((H(G)))) [insertion] (((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G)))) [iteration] (((AB(A))((...


7

23 steps (-a) * (-a) = ((-a) * (-a)) + 0 ✔ axiom 2 = ((-a) * (-a)) + (((-a) * a) + -((-a) * a)) ✔ axiom 3 = (((-a) * (-a)) + (-a) * a) + -((-a) * a) ✔ axiom 1 = (-a) * (-a + a) + -((-a) * a) ✔ axiom 8 = (-a) * (a + (-a)) + -((-a) * a) ...


7

6 + 7 + 7 + 6 + 3 = 29 steps I really hope I didn't screw anything up, leave a comment if you think I did. Lemma 1. a*0=0 (6 steps) 0 = a*0 + -(a*0) axiom 3 = a*(0+0) + -(a*0) axiom 2 = (a*0 + a*0) + -(a*0) axiom 8 = a*0 + (a*0 + -(a*0)) axiom 1 = a*0 + 0 axiom 3 = a*0 axiom 2 Lemma 2. a*(-b) = -(a*b) (7 steps) a*(-b) = a*(-b) + 0 axiom 2 = a*(-b) + (a*...


6

Score: 81 Each line should be worth 1 point. The De Morgan's laws are found at statements (3) and (6). Labels in brackets denote the previous statement(s) a line depends on if they are not immediately preceding. (a) assume P { (aa) P ^ P (ab) P (ac) P v Q } (a1) P -> P (a2) P -> P v Q (1) assume ~P ^ ~Q { (1a) assume P v Q { ...


5

34 steps Lemma 1: 0=0*a (8 steps) 0 A3: a*0 + -(a*0) A4: -(a*0) + a*0 A2: -(a*0) + a*(0+0) A8: -(a*0) + (a*0 + a*0) A1: (-(a*0) + a*0) + a*0 A3: 0 + a*0 A4: a*0 + 0 A2: a*0 Theorem: -a*-a = a*a (49 steps) -a * -a A2: (-a+0) * -a A2: (-a+0) * (-a+0) A3: (-a+(a+-a)) * (-a+0) A3: (-a+(a+-a)) * (-a+(a+-a)) A8: -a*(-a+(a+-a)) + (a+-a)*(-a+(a+-a)) A8: -...


5

304 steps Community wiki because this proof is generated by Mathematica's FindEquationalProof function. The proof is rather long. Mathematica doesn't know how to golf it. This is the Mathematica code that generates the proof (requires Mathematica 11.3), where p, t, n means +, ×, - respectively: ringAxioms = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], ...


5

25 steps Note: based on the question, I'm assuming that the rules of logic (including equality) are implied and do not count towards the total step count. That is, things like "if x=y, then y=x" and "if ((P AND Q) AND R) then (P AND (Q AND R))" can be used implicitly. Lemma Z [6 steps]: 0*a = 0: 0 = (0*a) + (-(0*a)) | Ax. 3 = ((0+0)*a) + (-(0*a)) ...


4

22 Steps \$\to\$(((())(()))) [Double Cut x3] \$\to\$(((AB())(CDE(F)()))H(G)) [Insertion x3] \$\to\$(((AB(A))(CDE(F)(CD(F)))(G))H(G)) [Iteration x3] \$\to\$(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G)))) [Double Cut x5] \$\to\$(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G)))) [Iteration] \$\to\$(((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(...


4

22 23 Steps New answer, as my previous was flawed. Let me add some general comments first: The problem does not allow to add terms on both sides of an equation; rather, we can only modify an initial string. Multiplication is not assumed to be commutative. We are given a unit 1, but it plays no role whatsoever in the puzzle because it is involved ...


4

Score: 59 Explanation I'll use a tree like structure for the proof as I find this style quite readable. Each line is annotated by the count of used rules, for example the "Example 1" in the challenge would be represented as this tree (growing bottom to top): Note the unknown counts A,B and also the assumption Γ - so this is no theorem. To demonstrate how ...


1

Score: 65 The de Morgan laws are line 30 and line 65. (I haven't made any particular effort to golf this, for example to see if there are some repeated proofs that could be abstracted out at the beginning.) 1. assume ~(P\/Q) 2. assume P 3. P\/Q by or-introl, 2 4. P -> P\/Q by impl-intro, 2, 3 5. P -> ~(P\/Q) by impl-intro, 2, 1 6. ...


Only top voted, non community-wiki answers of a minimum length are eligible