Post #2735442
2026-04-22 10:19 UTC
@byorgey@mathstodon.xyz nice! How does it compare to the implementation I made for agda-stdlib? https://agda.github.io/agda-stdlib/master/Data.Nat.Primality.Factorisation.html
Replies (1)
-
@byorgey@mathstodon.xyz 2026-04-22 17:07
@Taneb@hacksrus.xyz Oh, did you make that? Nice! I didn't look at it while I was writing mine, but I did find it to compare once I was finished. The proofs are pretty similar in broad outlines, as one might expect, but yours is definitely more efficient: for example, to test whether a number has a factor I simply try every possible divisor less than it; my proof makes no attempt to stop when reaching the square root, as yours does.