After more than a month of working with Aristotle of Harmonic, I’m reasonably confident that we’ve shown either in Lean or in Pari/gp enough to justify the statement: Let q<57000 be an odd prime such that 4q=a^2+27 for some positive integer a. Let N be an odd prime such that N=/=q and gcd(a,N)=1. Let s1… Continue reading Conjecture Verified in Lean for q<57000