Prove DeMorgan's laws
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 -&gt; P
  (a2) P -&gt; P v Q
(1) assume ~P ^ ~Q {
    (1a) assume P v Q {
        (1aa) assume Q {
            (1aaa) assume ~P {
                (1aaaa) Q ^ Q [1aa]
                (1aaab) Q
                (1aaac) ~Q [1]
            } (1aaa1) ~P -&gt; Q
              (1aaa2) ~P -&gt; ~Q
            (1aab) P
        } (1aa1) Q -&gt; P
        P [1a, a1, 1aa1]
        ~P [1]
    } (1a1) P v Q -&gt; P
      (1a2) P v Q -&gt; ~P
    (1b) ~(P v Q)
} (11) ~P ^ ~Q -&gt; ~(P v Q)
(2) assume ~(P v Q) {
    (2a) ~(P v Q) ^ ~(P v Q)
    (2b) assume P {
        (2aa) ~(P v Q) [2a]
    } (2b1) P -&gt; ~(P v Q)
    (2c) ~P [a2, 2b1]
    (2d) assume Q {
        (2da) ~(P v Q) [2a]
        (2db) P v Q
    } (2d1) Q -&gt; ~(P v Q)
      (2d2) Q -&gt; P v Q
    (2e) ~Q
    (2f) ~P ^ ~Q
} (21) ~(P v Q) -&gt; ~P ^ ~Q
(3) ~(P v Q) == ~P ^ ~Q [11, 21]
(4) assume ~P v ~Q {
    (4a) assume ~P {
        (4aa) assume P ^ Q {
            (4aaa) P
            (4aab) ~P ^ ~P [4a]
            (4aac) ~P
        } (4aa1) P ^ Q -&gt; P
          (4aa2) P ^ Q -&gt; ~P
        (4ab) ~(P ^ Q)
    } (4a1) ~P -&gt; ~(P ^ Q)
    (4b) assume ~Q {
        (4ba) assume P ^ Q {
            (4baa) Q
            (4bab) ~Q ^ ~Q [4b]
            (4bac) ~Q
        } (4ba1) P ^ Q -&gt; Q
          (4ba2) P ^ Q -&gt; ~Q
        (4bb) ~(P ^ Q)
    } (4b1) ~P -&gt; ~(P ^ Q)
    (4c) ~(P ^ Q) [4, 4a1, 4b1]
} (41) ~P v ~Q -&gt; ~(P ^ Q) 
(5) assume ~(P ^ Q) {
    (5a) assume ~(~P v ~Q) {
        (5aa) ~(~P v ~Q) ^ ~(P ^ Q) [5, 5a]
        (5ab) assume ~P {
            (5aba) ~P v ~Q
            (5abb) ~(~P v ~Q) [5aa]
        } (5ab1) ~P -&gt; ~P v ~Q
          (5ab2) ~P -&gt; ~(~P v ~Q)
        (5ac) P
        (5ad) assume ~Q {
            (5ada) ~P v ~Q
            (5adb) ~(~P v ~Q) [5aa]
        } (5ad1) ~Q -&gt; ~P v ~Q
          (5ad2) ~Q -&gt; ~(~P v ~Q)
        (5ae) Q
        (5af) P ^ Q [5ac, 5ae]
        (5ag) ~(P ^ Q) [5aa]
    } (5a1) ~(~P v ~Q) -&gt; P ^ Q
      (5a2) ~(~P v ~Q) -&gt; ~(P ^ Q)
    (5b) ~P v ~Q
} (51) ~(P ^ Q) -&gt; ~P v ~Q
(6) ~(P ^ Q) == ~P v ~Q [41, 51]