QUOD erat demonstrandum (QED): meaning "which was to be shown" has been used to end a formal proof of a mathematical proposition. Some mathematicians use a black square instead of QED. In UP, there's a professor (I forgot his name), who uses T.N. instead. T.N. means "tapos na". :)
The QED manifesto describes a project that aims to automate doing formal proofs using a computer. The four-color problem is the most famous theorem proved using a computer generated proof. I'm not quite sure how feasible this project is -- proving that a program has no bugs is in fact difficult.
Now, how can you prove that a computer program P which proves a theorem to be true has no bugs? Write another program Q that proves P has no bugs? I'm now confused. :)
No comments:
Post a Comment