Quantum Formalism (QF) Academy

Making Abstract Mathematics Accessible Since 2020.

Formalization: Proving Theorems via Computers

$$\neg [\forall x P(x)]\implies \exists x [\neg P(x)]. $$

Register to join

Abstract

Formalization of mathematics seeks to formally verify and prove mathematical statements using (interactive) proof assistants. In this talk, I will explore the motivations behind formalization and the key computer science concepts underlying it. I will also discuss current applications in mathematics and future possibilities, including the role of AI in future mathematical research. No specialized knowledge of mathematics or computer science is required—just a healthy curiosity. Everyone is welcome to attend!

Who Should Attend?

  • Anyone interested in this topic is welcome, especially researchers and engineers in AI, ML, and Quantum Computing.

Webinar Details:

📅 Date & Time: Monday, March 17 at 5PM GMT.

Register to join

About Dr. Nima Rasekh (The Speaker)

Claudia's Photo

Nima earned his PhD in Mathematics from the University of Illinois under the supervision of Prof. Charles Rezk and is currently a postdoctoral fellow at Uni Greifswald. Part of his research focuses on making complex mathematics, particularly (higher) category theory, more accessible through computers and formalization. In recent years, he has contributed to various efforts exploring advanced mathematics, via proof assistants such as Coq, Lean, and Rzk. He is passionate about sharing his experiences and learning from new perspectives.