London Futurists cover image

Provably safe AGI, with Steve Omohundro

London Futurists

CHAPTER

Exploring Mathematical Proof for Safe AI and Verified Code

In this chapter, the hosts discuss the possibility of organizing a conference or strand at AI conferences to explore the use of mathematical proof for safe AI. They mention the tool called Lean developed by Microsoft, which encodes all of mathematics and has the undergraduate curriculum and leading edge theorems formalized. They also talk about the progress in the field of formal methods for showing software correctness and the emerging trend of generating verified code along with the proofs. They conclude with the hope that these advancements can lead to a probably correct, probably safe version of technology that is controllable and beneficial for humanity.

00:00
Transcript
Play full episode

Remember Everything You Learn from Podcasts

Save insights instantly, chat with episodes, and build lasting knowledge - all powered by AI.
App store bannerPlay store banner