Past Events
2024
joined the Language Technology Institute at Carnegie Mellon.
Avigad and Marijn Heule taught in the Spring.
The Center hosted collaborative visits from and 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 .
"Formal Verification of the Empty Hexagon Number," by Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro and Marijn Heule, was accepted to .
"Teaching mathematics using Lean and controlled natural language," by Patrick Massot, was accepted to .
"Incorporating a database of graphs into a proof assistant," by Andrej Bauer, Katja Berčič, Gauvain Devillez, and Jure Taslak, was accepted to .
Mario Carneiro worked on , a formalization of Lean's metatheory in Lean.
2023
Jeremy Avigad gave a on formal mathematics at the Joint Mathematics Meetings in January 2023.
Joshua Clune's 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 .
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 in February.
"," 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.
"," by Alexander Bentkamp, Ramon Fernández Mir, and Avigad on appeared in TACAS 2023.
Quanta magazine published an about a combinatorial problem that was solved by Bernardo Subercaseaux and Heule with the help of a SAT solver.
Avigad gave a 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 on Lean at the in June.
Also in June, Avigad gave a talk and served on a panel at a National Academies workshop, "."
Avigad, Heule, and the Hoskinson Center were featured in an 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 .
A paper by Mario Carneiro, "Reimplementing Mizar in Rust," appeared in .
A paper by Carneiro, Chad Brown, and Josef Urban, "Automated Theorem Proving for Metamath," appeared in .
A paper by Avigad, Lior Goldberg, David Levit, Yoav Seginer and Alon Titelman, "A Proof-Producing Compiler for Blockchain Applications," appeared in .
A paper by Nawrocki, Edward Ayers and Gabriel Ebner, "An extensible user interface for Lean 4," appeared in .
"," by Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers, appeared in Tableaux 2023.
Avigad and worked on applications of Lean to teaching.
Undergraduate researcher Zachary Battleman worked on applications of Lean to software verification.
Joshua Clune worked on a that is currently in use at Amazon Web Services.
Starting in September, The Hoskinson Center hosted a year-long visit by , 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 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 and Oskar Abrahamsson. They about their work on Candle, a verified implementation of HOL Light.
The center hosted a six-month visit from PhD student (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 , 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 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 (Yale) to work on 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, , which was held at the 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 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 .
In the fall of 2022, Avigad and Marijn Heule taught , 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 .
The center hosted a visit by 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 . You can also watch and from the inauguration of the center. The slides that went with Avigad's presentation are .
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, , based on Lean 4.