Anand Rao Tadipatri

Name:	Anand Rao Tadipatri
Affiliation:	University of Cambridge, United Kingdom
E-mail:	(only provided to users who are logged into talks.cam)
Last login:	2 Mar 2026, 4:32 p.m.

Public lists managed by Anand Rao Tadipatri

• Formalisation of mathematics with interactive theorem provers

Talks given by Anand Rao Tadipatri

Obviously this only lists talks that are listed through talks.cam. Furthermore, this facility only works if the speaker's e-mail was specified in a talk. Most talks have not done this.

Talks organised by Anand Rao Tadipatri

This list is based on what was entered into the 'organiser' field in a talk. It may not mean that Anand Rao Tadipatri actually organised the talk, they may have been responsible only for entering the talk into the talks.cam system.

• Title to be confirmed
• The Serre finiteness theorem in Cubical Agda
• Certifying Synthetic Mathematics in Lean
• HoTTLean: Semantics of HoTT in Lean
• Aristotle, an AI theorem prover using Lean
• Lean4Less: Translating Lean to Smaller Theories via an Extensional-to-Intensional Translation
• Integrating Formal and Informal Reasoning
• Lambda-Superposition for Successful Hammering
• A Lean Tactic to Automatically Generalize Proofs
• Algebraic Geometry in Mathlib
• How to teach Fourier analysis to a large library of formalised mathematics
• A tour in (formalised) type theory
• New Foundations: the story of a large formalisation project
• Computer environments for math problem solving
• Alpha-Beta Pruning Explored, Extended and Verified
• Teaching using a proof assistant and controlled natural language
• Can a computer judge interestingness?
• Formalising Theory of Combinatorial Optimisation
• Formalising (part of) the Diagonal Ramsey Paper
• The Mandelbrot set is connected (and other Lean explorations)
• Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry
• How to prove Fermat's Last Theorem
• Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean
• Towards Autoformalization and Mathematical Reasoning using language models
• Title to be confirmed
• Title to be confirmed