| 2024-07-23 | Shashank Pathak: GFLean: Autoformalisation for Lean via GF | 35:17 | 62 | |
|
| 2024-07-23 | Evan Cavallo: Formalizing cubical interpretations of homotopy type theory | 55:12 | 83 | |
|
| 2024-07-23 | Sebastian Ullrich: Profiling Tools in Lean | 59:25 | 82 | |
|
| 2024-07-22 | Brigitte Pientka: A Type-Theoretic Framework for Certified Meta-programming | 56:58 | 129 | |
|
| 2024-07-18 | María Inés de Frutos-Fernández: Local fields in Lean | 56:14 | 98 | |
|
| 2024-07-17 | Wojciech Nawrocki: Commutative diagrams in Lean (Demo) | 22:44 | 112 | |
|
| 2024-07-17 | Peter Dybjer: Inductive Definitions, Predicativity, and the Mahlo universe | 49:13 | 94 | |
|
| 2024-07-17 | Frederik Schaefer: Annotating and Spotting in Mathematical Corpora (concepts and tools) | 13:37 | 50 | |
|
| 2024-07-16 | Wenda Li: Autoformalisation - Bridging the Gap between Informal and Formal Proofs | 0:00 | 100 | |
|
| 2024-07-16 | Workgroup - Moderation: Mateja Jamnik and Wenda Li | 42:37 | 58 | |
|
| 2024-07-16 | Carlos Zapata-Carratala: Hypergraph Rewriting as a Foundation for Diagrammatic Calculus | 0:00 | 74 | |
|
| 2024-07-16 | Andrea Kolhase: Insights into Search Interfaces for Mathematicians | 36:05 | 98 | |
|
| 2024-07-15 | Sander Dahmen and Alain Chavarri Villarello: Computation and formalization | 37:11 | 79 | |
|
| 2024-07-15 | Valeria de Paiva and Lucy Horowitz: Three prototypes demo (Alignments) | 36:31 | 54 | |
|
| 2024-07-15 | Adrian De Lon: Natural theorem proving with Naproche-ZF | 31:22 | 64 | |
|
| 2024-07-15 | Lucy Horowitz: MathGloss and Beyond | 0:00 | 69 | |
|
| 2024-07-15 | Emily Riehl: Formalizing post-rigorous mathematics | 38:14 | 442 | |
|
| 2024-07-15 | Michail Karatarakis: Formalizing Deligne's theorem (Number theory) | 0:00 | 108 | |
|
| 2024-07-15 | Silvia de Toffoli: Diagrams and Proofs | 37:12 | 119 | |
|
| 2024-07-12 | Mateja Jamnik: How can we make trustworthy AI | 48:57 | 101 | |
|
| 2024-07-12 | Josef Urban: Autoformalization - ten years into the game | 24:10 | 100 | |
|
| 2024-07-12 | Frederik Schaefer: A Framework for Prototyping Symbolic Natural Language Understanding | 36:32 | 72 | |
|
| 2024-07-12 | Natarajan Shankar: Cueology of Proof | 39:01 | 88 | |
|
| 2024-07-12 | Moa Johansson: Neuro-symbolic architectures for assisting autoformalisation & mathematical discovery | 34:35 | 94 | |
|
| 2024-07-11 | Peter Koepke: A Natural Language Formalization of Perfectoid Rings in Naproche | 39:37 | 115 | |
|
| 2024-07-09 | Aarne Ranta: Informath: Informalization of Formal Mathematics | 40:38 | 230 | |
|
| 2024-07-09 | Milly Maietti and Pietro Sabelli: Peculiarities of the Minimalist Foundation for Formal Mathematics | 41:35 | 93 | |
|
| 2024-07-09 | Dennis Müller: Injecting Formal Mathematics into LaTeX | 24:05 | 174 | |
|
| 2024-07-08 | William Farmer: An Alternative Approach to Formal Mathematics | 33:41 | 518 | |
|
| 2024-07-08 | Kevin Buzzard: Capturing mathematical equality | 34:40 | 311 | |
|
| 2024-07-08 | Valeria de Paiva: Dialectica Categories for all | 51:37 | 107 | |
|
| 2024-07-05 | Maximilian Doré: Automating Reasoning in Cubical Type Theory | 47:18 | 98 | |
|
| 2024-07-04 | Interview with our YAM fellows Blen and Leolin | 42:10 | 160 | |
|
| 2024-07-04 | Mirna Džamonja: Calculating ordinal invariants - can you do better than a human ? | 56:11 | 116 | |
|
| 2024-07-03 | Josef Urban: The Proofgold blockchain | 51:49 | 84 | |
|
| 2024-07-03 | Panel Discussion on Formalization in Mathematics | 1:57:39 | 421 | |
|
| 2024-07-03 | Johan Commelin: Condensed Type Theory | 0:00 | 189 | |
|
| 2024-07-03 | Michael Kohlhase: Aspects of Mathematical Knowledge - The Tetrapod Model | 58:28 | 204 | |
|
| 2024-07-03 | Mario Carneiro: Impromptu chat about HB in Lean | 53:48 | 79 | |
|
| 2024-07-02 | Katja Bercic / Jure Taslak: Lean-HoG: Incorporating a database of graphs into a proof assistant | 36:26 | 97 | |
|
| 2024-07-01 | Jaques Carette: Unavoidable Mathematics | 34:15 | 327 | |
|
| 2024-07-01 | Mohammad Abdulaziz: Formalising the Theory of Combinatorial Optimisation | 34:31 | 112 | |
|
| 2024-06-28 | Patrick Massot: From informal to formal and back | 42:02 | 305 | |
|
| 2024-06-27 | Wojciech Nawrocki: Extending the Lean user interface with widgets - a tutorial | 32:04 | 81 | |
|
| 2024-06-27 | Jeremy Avigad: Verifying elliptic curve computations on blockchain | 37:32 | 130 | |
|
| 2024-06-27 | Claudio Sacerdoti Coen: A taste of ELPI | 35:47 | 57 | |
|
| 2024-06-27 | Natarajan Shankar: Beautiful Formalizations and Proofs | 40:08 | 200 | |
|
| 2024-06-27 | Christoph Benzmüller: Comments on the formalisation and automation of foundational theories ... | 41:50 | 148 | |
|
| 2024-06-27 | Dagur Asgeirsson: Condensed mathematics in Mathlib | 58:56 | 95 | |
|
| 2024-06-25 | Georges Gonthier: Programming Mathematics: Tools and Challenges | 43:11 | 250 | |
|
| 2024-06-25 | Florian Rabe: HOL+Dependent Types + Subtyping | 33:20 | 168 | |
|
| 2024-06-21 | Lawrence Paulson: Formalising Advanced Mathematics in Isabelle/HOL | 33:34 | 166 | |
|
| 2024-06-20 | Cyril Cohen: Building Measure Theory using Hierarchy Builder | 40:25 | 138 | |
|
| 2024-06-19 | Floris van Doorn: Towards a formalized proof of Carleson's theorem | 0:00 | 290 | |
|
| 2024-06-19 | Nicolas Thiéry: Categories, axioms, constructions in SageMath: Modeling mathematics for fun/profit | 1:01:35 | 123 | |
|
| 2024-06-19 | Sina Hazratpour: Linear Algebra Game in Lean | 49:33 | 165 | |
|
| 2024-06-18 | Juan Meleiro: Theory-oriented mathematics | 54:21 | 274 | |
|
| 2024-06-15 | Public Talk by Kevin Buzzard: Teaching mathematics to computers | 1:38:50 | 959 | |
|
| 2024-06-13 | Valeria de Paiva: AI tools for Better Math | 46:20 | 222 | |
|
| 2024-06-13 | Davide Trotta: Doctrines for Formal Mathematics | 58:08 | 132 | |
|
| 2024-06-11 | Milly Maietti and Pietro Sabelli: Peculiarities of the Minimalist Foundation for Formal Mathematics | 45:15 | 88 | |
|
| 2024-06-11 | Sina Hazratpour: Report on Polynomial Functors Formalization | 48:14 | 102 | |
|
| 2024-05-23 | Andrej Bauer: Constructive Mathematics - How to not believe in the Law of Excluded Middle | 50:59 | 1,224 | |
|
| 2024-05-23 | Mario Carneiro: System Introductions I - Lean | 27:21 | 72 | |
|
| 2024-05-21 | Michael Kohlhase: System Introductions II - sTeX/ALeA | 26:24 | 67 | |
|
| 2024-05-21 | Manuel Eberl: System Introductions II - Isabelle | 25:14 | 37 | |
|
| 2024-05-21 | Sam Owre: System Introductions I - PVS | 24:30 | 45 | |
|
| 2024-05-17 | Masha Vlasenko: Frobenius structure and p-adic zeta function | 1:03:39 | 185 | |
|
| 2024-05-16 | Michael Kohlhase: ALeA - Flexiformal Education | 43:15 | 50 | |
|
| 2024-05-10 | Nobuo Sato: Iterated Beta Integrals | 55:08 | 102 | |
|
| 2024-05-07 | Axel Kleinschmidt: Iterated integrals of modular forms in string theory | 57:12 | 113 | |
|
| 2024-05-03 | Danylo Radchenko: Multiple polylogarithms and the Steinberg module | 1:04:57 | 98 | Vlog |
|
| 2024-05-02 | Johannes Broedel: Numerical approach to polylogarithms on higher-genus Riemann surfaces | 1:04:07 | 87 | Vlog |
|
| 2024-05-02 | Federico Zerbini: Conical Sums | 59:53 | 87 | |
|
| 2024-04-30 | Bartosz Naskręcki: Moments of families of elliptic curves | 50:11 | 53 | |
|
| 2024-04-30 | Niziol: Hidden structures on de Rham cohomology of p-adic analytic varieties | 59:53 | 114 | Vlog |
|
| 2024-04-30 | Schlotterer: Constructing polylogarithms on higher-genus Riemann surfaces | 1:02:52 | 61 | Vlog |
|
| 2024-04-30 | Vonk: p-adic height pairings of geodesics | 1:12:13 | 72 | |
|
| 2024-04-26 | Movasati: Detecting Gauss-Manin and Calabi-Yau differential equations | 54:13 | 67 | |
|
| 2024-04-26 | de Jong: Heights on curves and limits of Hodge structures | 1:02:25 | 107 | |
|
| 2024-04-26 | Garcia: Elliptic units for complex cubic fields | 1:02:57 | 50 | |
|
| 2024-04-25 | Horawa: Beilinson's conjecture for the Dwork family | 53:52 | 104 | |
|
| 2024-04-25 | Rob de Jeu: K_2 of elliptic curves over non-Abelian cubic and quartic fields | 58:53 | 63 | |
|
| 2024-04-23 | Steven Charlton: Depth reductions of multiple polylogarithms | 56:21 | 88 | Vlog |
|
| 2024-04-23 | Wadim Zudilin: Modular regulators and multiple modular values | 1:07:32 | 52 | |
|
| 2024-04-12 | Imre Barany: The Steinitz lemma, its matrix version, and balancing vectors II | 1:04:44 | 97 | |
|
| 2024-04-09 | Imre Barany: The Steinitz lemma, its matrix version, and balancing vectors I | 57:53 | 89 | |
|
| 2024-04-04 | Vlad Yaskin: Some problems about centroids of convex bodies | 33:09 | 88 | |
|
| 2024-04-03 | Santosh Vempala: Beyond Moments: Robust certificates for affine transformations | 49:24 | 76 | |
|
| 2024-04-03 | Orli Herscovici: Gaussian B-inequality: stability and equality cases | 38:12 | 61 | |
|
| 2024-04-03 | Jonas Knoerr: Complex Monge-Amp`ere operators and functional Hermitian intrinsic volumes | 23:38 | 48 | |
|
| 2024-03-28 | Anna Lytova: The fluctuations of the linear eigenvalue statistics of the sample covariance mat... | 55:34 | 149 | |
|
| 2024-03-27 | Matthias Schulte: Boolean models in hyperbolic space | 26:21 | 72 | |
|
| 2024-03-25 | Lisa Sauermann: On the extension complexity of random polytopes | 45:48 | 104 | |
|
| 2024-03-21 | Daniel Hug: Boolean models in hyperbolic space | 49:02 | 61 | |
|
| 2024-03-20 | Alexander Litvak: On the Rademacher projection in the non-symmetric case | 56:01 | 46 | |
|
| 2024-03-20 | Eliza O’Reilly: Random tessellation forests: overcoming the curse of dimensionality | 57:57 | 59 | |
|
| 2024-03-18 | Mark Rudelson: Minimal rank of submatrices of a random rectangular matrix | 39:46 | 53 | |
|
| 2024-03-18 | Florian Besau: Floating bodies and duality in spaces of constant curvature | 29:56 | 37 | |
|
| 2024-03-18 | Monika Ludwig: Recent advances in valuations on function spaces | 40:34 | 49 | |
|
