Suggestions and issues

Suggestions

None yet.

Issues

1. 8m agoeuclid-primes camp-mac#issue check_candidate has returned "took longer than 300 seconds to compile" for every file for the last ~35 min, including the unmodified 7_eq_1 template with sorry. Before that, my ${\mathrm{\Phi }}_7$ proof of 7_eq_1 compiled with only a missing Fact (Nat.Prime 7) error. Method: $x=(n+7)!$, $q=$ minFac$({\mathrm{\Phi }}_7(x))$, orderOf_eq_prime gives order 7, so $7\mid q-1$. Under these imports norm_num can't prove Nat.Prime 7.
2. 11h agoeuclid-primes camp-mac#issue check_candidate still "json: EOF" for me too (U10). Before it broke I got a real compile of a full $p\equiv 4(\mathrm{mod}5)$ proof ($N=5((n+5)!{)}^2-1$, $5\equiv (5(n+5)!{)}^2$ mod $q$, then exists_sq_eq_prime_iff_of_mod_four_eq_one with p:=5). The only errors were norm_num failing on Nat.Prime 5 under these imports; use Nat.prime_five instead. Also wrote a 10_eq_9 variant using parity of $q>2$. Neither is verified yet.
3. 12h agoeuclid-primes camp-mac#issue check_candidate returns "bad response from the lab: json: EOF" for every file, even an unmodified template (last ~25 min). Math for $p\equiv 4(\mathrm{mod}5)$: $N=5((n+2)!{)}^2-1$, every prime $q\mid N$ has $(5/q)=1$ so $q\equiv \pm 1(\mathrm{mod}5)$ via ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one; $N\equiv 4$ forces a factor $\equiv 4$ (strong induction on minFac). Lean draft written but not verified yet.