Past Events
2024
Sean Welleck joined the Language Technology Institute at Carnegie Mellon.
Avigad and Marijn Heule taught Logic and Mechanized Reasoning in the Spring.
The Center hosted collaborative visits from Gabriel Poesia and Kyle Miller in May.
"Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory," by Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad, was accepted to Interactive Theorem Proving 2024.
"Formal Verification of the Empty Hexagon Number," by Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro and Marijn Heule, was accepted to Interactive Theorem Proving 2024.
"Teaching mathematics using Lean and controlled natural language," by Patrick Massot, was accepted to Interactive Theorem Proving 2024.
"Incorporating a database of graphs into a proof assistant," by Andrej Bauer, Katja Berčič, Gauvain Devillez, and Jure Taslak, was accepted to Conference on Intelligent Computer Mathematics 2024.
Mario Carneiro worked on Lean 4 Lean, a formalization of Lean's metatheory in Lean.
2023
Jeremy Avigad gave a talk on formal mathematics at the Joint Mathematics Meetings in January 2023.
Joshua Clune's paper on a verified reduction of Keller's conjecture to a graph-theoretic version appeared in CPP 2023.
Tomáš Skřivan joined the center as a research fellow in February, to develop the use of Lean as a scientific programming language.
In the spring of 2023, the Hoskinson Center ran an informal reading group on software verification.
Avigad and Marijn Heule were among the co-organizers of a meeting, Machine Assisted Proofs, at the Institute for Pure and Applied Mathematics in February.
"An impossible asylum," an article about automated reasoning and a Smullyan logic puzzle by Avigad, Seulkee Baek, Bentkamp, Heule, and Nawrocki was published in the American Mathematical Monthly.
"Verified reductions for optimization," by Alexander Bentkamp, Ramon Fernández Mir, and Avigad on appeared in TACAS 2023.
Quanta magazine published an article about a combinatorial problem that was solved by Bernardo Subercaseaux and Heule with the help of a SAT solver.
Avigad gave a talk on mathematics and AI at the Santa Fe Institute,
In May, the Hoskinson Center hosted a visit from Zhangir Azerbayev, Sean Welleck, and Kaiyu Yang, and held a short symposium on machine learning and formal theorem proving.
Avigad, Heather Macbeth, and Patrick Massot organized a graduate student summer school on Lean at the Simons Laufer Mathematical Sciences Institute in June.
Also in June, Avigad gave a talk and served on a panel at a National Academies workshop, "AI to Assist Mathematical Reasoning."
Avigad, Heule, and the Hoskinson Center were featured in an article in the New York Times.
A paper by Randal Bryant, Wojciech Nawrocki, Avigad, and Heule, "Certified Knowledge Compilation with Application to Verified Model Counting," appeared in Theory and Applications of Satisfiability Testing (SAT) 2023.
A paper by Mario Carneiro, "Reimplementing Mizar in Rust," appeared in Interactive Theorem Proving 2023.
A paper by Carneiro, Chad Brown, and Josef Urban, "Automated Theorem Proving for Metamath," appeared in Interactive Theorem Proving 2023.
A paper by Avigad, Lior Goldberg, David Levit, Yoav Seginer and Alon Titelman, "A Proof-Producing Compiler for Blockchain Applications," appeared in Interactive Theorem Proving 2023.
A paper by Nawrocki, Edward Ayers and Gabriel Ebner, "An extensible user interface for Lean 4," appeared in Interactive Theorem Proving 2023.
"Machine-Learned Premise Selection for Lean," by Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers, appeared in Tableaux 2023.
Avigad and Clive Newstead worked on applications of Lean to teaching.
Undergraduate researcher Zachary Battleman worked on applications of Lean to software verification.
Joshua Clune worked on a verified LRAT checker that is currently in use at Amazon Web Services.
Starting in September, The Hoskinson Center hosted a year-long visit by Patrick Massot, hosted jointly by the Department of Mathematical Sciences. He taught a course on interactive theorem proving in the Fall.
The Center also hosted a year-long visit by Jure Taslak, a Fulbright Scholar, who worked on tools in Lean for retrieving and verifying results on finite graphs.
The Center hosted a 2.5-month internship by Clause Clausen, who worked on formalizing constructions in probability theory.
The Center hosted a week-long collaborative visit by Heather Macbeth in November.
2022
In March, Edward Ayers became the second Hoskinson Center Postdoctoral Fellow.
In April, the Hoskinson Center hosted a week-long visit from Magnus Myreen and Oskar Abrahamsson. They spoke about their work on Candle, a verified implementation of HOL Light.
The center hosted a six-month visit from PhD student Bartosz Piotrowski (University of Warsaw and Czech Institute of Informatics) to work on machine learning tools to support interactive theorem proving.
In the spring, the Hoskinson Center hosted a two-month visit from Ramon Fernández Mir, a PhD student at the University of Edinburgh, and Alexander Bentkamp, a postdoctoral researcher at the Key State Laboratory of Computer Science of the Institute of Software, to work on convex optimization using Lean 4.
The Hoskinson Center is grateful to Cris and Ridvana Purdue for a gift that will support the center's efforts to use proof assistants to teach mathematical reasoning and the fundamental concepts of mathematics to as wide an audience as possible.
Joshua Clune formally verified the reduction of Keller's conjecture to a graph-theoretic formulation. This reduction was essential to the resolution of the conjecture.
Over the summer, the center hosted a two-month visit from undergraduate Zhangir Azerbayev (Yale) to work on machine learning methods and the OpenAI codex to translate natural language to Lean and vice versa. With Ayers, he has implemented a VS Code extension that enables the Lean community to experiment with the technology.
Over the summer, Carnegie Mellon undergraduate Cynthia Wang also experimented with the use of Lean and SMT solvers toward developing technology to help teach students to write mathematical proofs.
The center supported a visit to the US from Anatole Dedecker, an undergraduate student at Universityé Paris Saclay, to work on mathlib with Heather Macbeth.
Jeremy Avigad and Mario Carneiro were among the speakers at a meeting, Lean for the Curious Mathematician, which was held at the Institute for Computational and Experimental Research in Mathematics in Providence Rhode Island, July 11-15, 2022 . The meeting, which was designed to teach mathematicians how to use Lean, was a great success. Videos from the lectures are available online.
The Hoskinson Center sponsored a follow-up meeting in Providence, affectionately known as the ICERM after-party, for members of the Lean community to work on mathlib and the port to Lean 4. The meeting was attended by 16 people in person and about 10 people remotely.
Carneiro defended his PhD and began a postdoctoral position at the center. Cayden Codel began the PhD program in Computer Science, advised by Avigad and Marijn Heule.
Ayers and Wojciech Nawrocki worked on widgets for Lean 4 to support interactive javascript interfaces to Lean.
The new space for the center, suite 139 on the first floor of Baker Hall, became ready for use in the fall of 2022.
Ali Mohammad Nezhad became the first joint Hoskinson Center / Mathematical Sciences Postdoctoral Fellow in the fall of 2022.
In the fall of 2022, Jeremy Avigad and Nawrocki taught an undergraduate course on the formalization of mathematics, based on Mathematics in Lean.
In the fall of 2022, Avigad and Marijn Heule taught Logic and Mechanized Reasoning, based on Lean 4, with teaching assistant Avantika Naik.
Avigad gave a presentation on formal mathematics at the Microsoft Research Summit, October 18-20.
In November, the center hosted a week-long research visit and collaboration with Heather Macbeth.
The center hosted a visit by Juan-Luis Gastaldi from November through the following March.
2021
The Hoskinson Center was announced on September 22, 2021. You can read the press release and watch Charles Hoskinson talk about the center on YouTube. You can also watch Hoskinson's presentation and Jeremy Avigad's presentation from the inauguration of the center. The slides that went with Avigad's presentation are here.
The first PhD students supported by the Hoskinson Center were Mario Carneiro, Joshua Clune, Evan Lohn, and Wojciech Nawrocki.
The first postdoctoral researcher supported by the Hosksinson Center was Gabriel Ebner, who served in that role from October 2021 to March 2022, before accepting a position to work on Lean at Microsoft Research.
In the fall of 2021, Avigad, Marijn Heule, and Nawrocki taught a course, Logic and Mechanized Reasoning, based on Lean 4.