A proof assistant is a computer program that takes as input a proof in a formal language and outputs true if and only if the proof is a valid proof in a formal system. An example would be first-order logic with its inference rules. Proof assistants are supposed to tell you whether your proof is […]
I happened to come across a 1993 opinion piece, Theorems for a price: Tomorrow's semi-rigorous mathematical culture by Doron Zeilberger. I think it's a rather fascinating document as it questions the future of mathematical proof. Its basic thesis is that some time in the future of mathematics, the expectation of proof will move to a […]
Is mathematics science or art? Mathematics resembles science. In math, data and examples are collected and hypotheses made. There is a difference in the hypotheses of math versus science: in the former they can be proved, but that could be considered a small point. But I have met mathematicians who don't consider themselves scientists, and […]
Three things I would like to see happen with the practice of mathematics in the next ten years are: Computer proof assistants… …that are easy to use for the typical mathematician. Why? Mathematics is expanding tremendously and some areas are getting quite abstract. Some areas are so complex that I even wonder if anyone in […]
Update: Voting is now closed. I've decided to add more interactivity to this blog. As a first step, I'd like to know what kinds of posts readers would like to see. So click an option and vote!
A senior mathematician who will remain nameless recently said in a talk, "there is nothing left to prove". In context, he was referring to the possibility that we are running out of math problems. People who heard laughed, and first-year calculus students might disagree. Was it said as a joke? Because of the infinite nature […]