Post #1666321
2026-04-22 12:36 UTC
This is the point of formalization:
In several places, the process of formalization sharpened our understanding
of the informal presentation.
p. 4 of a just-landed formalization of the reals in cubical agda. https://users.cs.utah.edu/~blg/resources/pdf/jackson-brough-cubicalreals-2026.pdf
Replies (2)
-
@rzeta0@mathstodon.xyz 2026-04-22 13:16
@JacquesC2 i'm a total beginner who dipped my toe into writing formal (simple) proofs in lean and yes, the process made me really clarify my understanding of the proof strategy and details that proof checkers are not forgiving of ambiguity or "read between the lines" was very educational for me
-
@ncf@types.pl 2026-04-22 16:43
@JacquesC2 "ON THE USE OF CLAUDE CODE" ffs