Fermat

[jhlchan]

Update algebra library, incorporate an improved algorithm for Fermat's Two Squares Theorem.

[mn200]

Unless there's strong reason to, please don't use paired existentials, like ?(a,b).... Instead, just have the existentially quantified variables listed: ?a b. ...

[jhlchan]

New commit uses simple existentially quantified variables. Should I worry about the failure of [d64379b]?

[jhlchan]

Got it. Now I learn how to read the log, and fixed the problem. Hope this is the only one.

[jhlchan]

This time it is the standard kernel, but I have used rename1 to ensure proper variable rename. Log seems not to fail in fermat/ folder. Any suggestion about the exact issue?

[jhlchan]

Thanks for all your help, much appreciated.

[mn200]

Failure (visible through link) is:

#13 3771.2  ∀n. n MOD 4 ≠ 0 ⇒ fixes zagier (mills n) = {(x,x,z) | n = windmill (x,x,z)}
#13 3771.2  
#13 3771.2  failed.
#13 3771.2  Failed to prove theorem zagier_fixes.
#13 3771.2  

This was in the experimental kernel where variable names chosen by the kernel can be different.

[mn200]

Still seem to be an issue?

[mn200]

That more recent error is not yours; it's a common repeated error that that file throws up non-deterministically.

Thanks for your work!