| HEAD | 0f249ef | Improve number07 proof This is starting to see diminishing returns, so I may not continue with these simplifications, but this was the next heavy hitter on the list of compile time records, so I thought I would take a look. There were some very silly proofs that e.g. the divisors of 226 are {1,2,113,226} which proceeded by testing all smaller numbers (where the better proof is to observe that 226 = 2*113 and these are prime). Replacing these with one line proofs resulted in the majority of the size reduction of the file. The second improvement is in the enumeration of all n <= 201 such that "n satisfies_Sierpinski_problem_89". The original proof first proved each case in a separate lemma, then tries to combine them 6 at a time. The problem is that "n satisfies_Sierpinski_problem_89" is defined as a conjunction of three things, so the verifier internally explodes each assumption "not 18 satisfies...", "not 19 satisfies..." etc into 3 cases each, resulting in 6 * 3^6 = 4374 cases being sent to the verifier after expansion and making this proof extremely slow. It turns out that only one in 4 cases actually need to be dealt with explicitly, the rest can be proven impossible without case analysis. Inlining the proofs of "not 18 satisfies..." etc also solves the case explosion problem. The net result: lines: 11310 -> 2267 (80% reduction) verifier: 11:05 -> 0:17 (39x improvement) mizar-rs: 1:24.5 -> 0:02.5 (34x improvement) | 27 April 2023, 10:44:05 UTC |
| refs/heads/itp2023 | f13f2ce | add files for ITP 2023 submission | 23 February 2023, 17:26:04 UTC |
| refs/heads/main | 0f249ef | Improve number07 proof This is starting to see diminishing returns, so I may not continue with these simplifications, but this was the next heavy hitter on the list of compile time records, so I thought I would take a look. There were some very silly proofs that e.g. the divisors of 226 are {1,2,113,226} which proceeded by testing all smaller numbers (where the better proof is to observe that 226 = 2*113 and these are prime). Replacing these with one line proofs resulted in the majority of the size reduction of the file. The second improvement is in the enumeration of all n <= 201 such that "n satisfies_Sierpinski_problem_89". The original proof first proved each case in a separate lemma, then tries to combine them 6 at a time. The problem is that "n satisfies_Sierpinski_problem_89" is defined as a conjunction of three things, so the verifier internally explodes each assumption "not 18 satisfies...", "not 19 satisfies..." etc into 3 cases each, resulting in 6 * 3^6 = 4374 cases being sent to the verifier after expansion and making this proof extremely slow. It turns out that only one in 4 cases actually need to be dealt with explicitly, the rest can be proven impossible without case analysis. Inlining the proofs of "not 18 satisfies..." etc also solves the case explosion problem. The net result: lines: 11310 -> 2267 (80% reduction) verifier: 11:05 -> 0:17 (39x improvement) mizar-rs: 1:24.5 -> 0:02.5 (34x improvement) | 27 April 2023, 10:44:05 UTC |
