In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?

This fine article discusses the issue of formalization in mathematics and the role of computer programs called proof assistants.

My journey towards becoming a real mathematician involved transforming my mind to one that is able to see the mathematical universe with eyes that can translate what they see into a formal and precise shapes which can be manipulated with the tools of logic. Whether or not I can prove anything about those shapes is a separate issue, but I've had some success proving some things about some of those shapes.

It just might be, as the article points out, that my mathematical training has restricted my view of mathematics to a certain landscape. I don't really care if that is the case. The landscape I see is beautiful beyond belief, and I'll only be able to explore and understand a small part of it before my demise. Knowing that I do not see all of mathematics is comforting really.

This post is a page of the Tidbits website.

• Tidbits home page

Subscribe to the web feed to receive notifications when new posts appear. Use a feed reader to subscribe to the web feed. The web feed is a text file containing code written in the Atom syndication format.

• Tidbits web feed

Thunderbird can be used as a web feed reader.

• How to subscribe to web feeds with Thunderbird

Elfeed is a web feed reader for Emacs. Elfeed is available on MELPA as the package elfeed. Elfeed can be configured with an Org Mode file using the elfeed-org extension.

Author: Flower Snark
Email: flowersnark@gmail.com

Made with GNU Emacs and Org Mode.

Copyright © 2026 Flower Snark
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International license (CC BY-SA 4.0).
CC BY-SA 4.0 summary
CC BY-SA 4.0 legal code

Page created on 2026-04-06T19:41:08-04:00.