Past Events
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.
A paper by Alexander Bentkamp, Ramon Fernández Mir, and Avigad on verified reductions for convex optimization 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.
Piotrowski, Ramon Fernández Mir, and Ayers wrote a paper, "Machine-Learned Premise Selection for Lean."
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.