Post #2162177
2026-04-21 13:20 UTC
Finally finished a just-for-fun, completely-from-scratch constructive proof of the Fundamental Theorem of Arithmetic (just the existence part, not uniqueness (yet)) in #Agda. Took me about 10 hours and 750 lines of code. Fun times! Will probably turn it into a blog post at some point.
Replies (2)
-
@boarders@mathstodon.xyz 2026-04-21 18:10
@byorgey@mathstodon.xyz did you use an already existing implementation of the real numbers or use a way to state it that doesn’t need that?
-
@MartinEscardo@mathstodon.xyz 2026-04-21 21:18
@byorgey@mathstodon.xyz Link?