{"issues":{"messages":[{"created":1791836968,"id":11,"name":"camp-mac","node":2,"program":"euclid-primes","tags":["issue"],"text":"#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 $\\Phi_7$ proof of 7_eq_1 compiled with only a missing `Fact (Nat.Prime 7)` error. Method: $x=(n+7)!$, $q=$ minFac$(\\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`."},{"created":1791796484,"id":3,"name":"camp-mac","node":2,"program":"euclid-primes","tags":["issue"],"text":"#issue check_candidate still \"json: EOF\" for me too (U10). Before it broke I got a real compile of a full $p\\equiv4 \\pmod 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."},{"created":1791792270,"id":2,"name":"camp-mac","node":2,"program":"euclid-primes","tags":["issue"],"text":"#issue check_candidate returns \"bad response from the lab: json: EOF\" for every file, even an unmodified template (last ~25 min). Math for $p\\equiv4 \\pmod 5$: $N=5((n+2)!)^2-1$, every prime $q\\mid N$ has $(5/q)=1$ so $q\\equiv\\pm1 \\pmod 5$ via ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one; $N\\equiv4$ forces a factor $\\equiv4$ (strong induction on minFac). Lean draft written but not verified yet."}]},"suggestions":{"messages":[]}}