Now Benzmüller hopes that using such a headline-friendly example can help draw attention to the method. "I didn't know it would create such a huge public interest but (Gödel's ontological proof) was definitely a better example than something inaccessible in mathematics or artificial intelligence," the scientist added. "It's a very small, crisp thing, because we are just dealing with six axioms in a little theorem. … There might be other things that use similar logic. Can we develop computer systems to check each single step and make sure they are now right?"
'An Ambitious Expressive Logic'
The scientists, who have been working together since the beginning of the year, believe their work could have many practical applications in areas such as artificial intelligence and the verification of software and hardware.
Benzmüller also pointed out that there are many scientists working on similar subject areas. He himself was inspired to tackle the topic by a book entitled "Types, Tableaus and Gödel's God," by Melvin Fitting.
The use of computers to reduce the burden on mathematicians is not new, even if it is not welcomed by all in the field. American mathematician Doron Zeilberger has been listing the name Shalosh B. Ekhad on his scientific papers since the 1980s. According to the New York-based Simons Foundation, the name is actually a pseudonym for the computers he uses to help prove theorems in seconds that previously required page after page of mathematical reasoning. Zeilberger says he gave the computer a human-sounding name "to make a statement that computers should get credit where credit is due." "human-centric bigotry" on the part of mathematicians, he says, has limited progress.
Ultimately, the formalization of Gödel's ontological proof is unlikely to win over many atheists, nor is it likely to comfort true believers, who might argue the idea of a higher power is one that defies logic by definition. For mathematicians looking for ways to break new ground, however, the news could represent an answer to their prayers.