The path to a superhuman AI mathematician

Wiskunde is waarschijnlijk het eerste domein waarin bewijs van AI-superintelligentie zichtbaar wordt, zegt theoretisch computerwetenschapper Sanjeev Arora. Voor de Communications of the Association for Computing Machinery (ACM) schreef ik over zijn ideeën.

Mathematics is the first place where evidence of AI superintelligence is likely to appear, theoretical computer scientist Sanjeev Arora says. For the Communications of the Association for Computing Machinery (ACM) I wrote about his ideas.

“Will there be a superhuman AI mathematician?” asked theoretical computer scientist professor Sanjeev Arora from Princeton University at the 12th Heidelberg Laureate Forum this September. Well, what would that mean? Imagine the set of all possible math theorems. Only a subset has been proven by human mathematicians. Arora: “A superhuman AI mathematician is one that can prove more theorems than humans have.”

Arora, who won the 2011 ACM Prize in Computing, sketched a possible path to a superhuman AI mathematician. He explained that the idea traces back to David Hilbert’s early 20th-century dream of automating mathematics. That dream was crushed by the work of Gödel, Turing, and Church, yet it left behind something lasting: the concept of formal proof verification — the notion that mathematical proofs can be written in a precise language and then rigorously checked by a computer.

The modern open-source programming language and proof assistant Lean is ideally suited for precisely this purpose, Arora told. A proof written in English can be translated into Lean after which the Lean checker verifies whether or not the proof is correct. Arora: “Rewriting the proof in Lean is presently done by humans, but very soon this will be done by AI.”

The whole article can be read on the ACM website.

Let a Digital Twin Predict Your Heart’s Health

In een artikel voor de Communications of the Association for Computing Machinery (ACM) laat ik zien hoe digitale tweelingen van het cardiovasculaire systeem in de toekomst hartproblemen kunnen voorspellen nog vóórdat je klachten hebt — dankzij simulaties van miljoenen hartslagen en data uit wearables. Prachtig onderzoek van Amanda Randles (Duke University, VS), winnaar van de 2023 ACM Prize in Computing:

In an article for the Communications of the Association for Computing Machinery (ACM), I show how vascular digital twins may soon predict heart problems long before symptoms appear — powered by simulations spanning millions of heartbeats and data from wearables. Beautiful research by Amanda Randles (Duke University, USA), winner of the 2023 ACM Prize in Computing:

At the 12th Heidelberg Laureate Forum this September, Amanda Randles reached a unique milestone: she is the first participant who attended the Forum first as a talented young researcher (in 2013) and returned to give a keynote lecture as a laureate of the ACM Prize in Computing. She won the 2023 prize for her work on “revolutionizing medical diagnostics”. 

Randles, who is now an associate professor of biomedical engineering at Duke University, is developing vascular digital twins: virtual replicas of a patient’s vascular system. They evolve over time with the patient and are partly informed by data from wearable devices. Her long-term vision is that, in the future, these digital twins will be used to predict and prevent disease, beginning with heart attacks.

The whole article can be read on the ACM website.