Skip to main content

Hoskinson Center announced

Announcements

On September 22, 2021, Carnegie Mellon University announced that a $20 million gift from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson Center for Formal Mathematics, housed in the Department of Philosophy. You can read the university press release and watch Hoskinson's YouTube announcement. You can also watch Hoskinson's presentation and my presentation at an inauguration ceremony that was held at Carnegie Mellon the day before. The slides I used for the presentation are here.

The center's mission is to support the work being done by the Lean community, to promote the use of Lean and its libraries, and to seek out ways of using the technology to make mathematics accessible and enjoyable to as wide an audience as possible.

The initial endowment will be used to support postdoctoral researchers and graduate students, as well as occasional meetings and visitors. In the near future, the center will focus on supporting the port of mathlib to Lean 4, developing automation and the user interface, and, perhaps most importantly, preparing textbooks and educational materials based on Lean.

Yury Kudryashov’s rotation number paper

Papers

Yury Kudryashov wrote a paper about the rotation number for the CICM 2021 conference on intelligent computer mathematics.

Rotation number is the key numerical invariant of an orientation preserving circle homeomorphism. Circle self-maps $f : S^1 → S^1$, $S^1 = ℝ/ℤ$, constitute an important class of dynamical systems. They appear in applications, e.g., as Poincaré maps of continuous flows on the $2$-torus. The simplest circle self-maps are pure rotations $x ↦ x + a$. It turns out that any circle homeomorphism f is semiconjugate to a pure rotation $x ↦ x + τ(f)$. The number $τ(f)$ is called the rotation number of $f$.

This paper describes the current state of an ongoing project with aim to formalize various facts about circle dynamics in Lean. Currently, the formalized material includes the definition and basic properties of the translation number of a lift of a circle homeomorphism to the real line. Yury Kudryashov also formalized a theorem by Étienne Ghys that gives a necessary and sufficient condition for two actions of a group on the circle by homeomorphism to be semiconjugate to each other.

Eric Wieser's scalar action paper

Papers

Eric Wieser wrote a paper about scalar actions in mathlib for the CICM 2021 conference on intelligent computer mathematics.

Scalar actions are everywhere in mathematics. There are so many of them that a given type can easily get several ones from different origins. For instance $ℤ$ acts on itself by left multiplication but it also has the $ℤ$ scalar action that every additive group has, by repeated addition or subtraction. In general those multiple actions can be proven to be equal, but type class inference needs definitional equality. So a great deal of care has been taken, by Eric and others, when setting up the algebraic hierarchy in mathlib.

The paper tells this fascinating story and is recommended for anyone interested in multiple inheritance handling in Lean 3 type class system.

Welcome to the Lean community blog!

Announcements

This is our brand new blog where you'll be able to find news about what is happening in the Lean prover community. It will feature:

  • posts highlighting some new contributions to mathlib
  • news about ongoing projects such as the Liquid tensor experiment or the sphere eversion project
  • news about exciting developments in other proofs assistants
  • announcements of conferences and talks
  • some explanations of specific topics in a less formal context than the documentations
  • speculations about future developments or somewhat philosophical discussions

There is no predefined list of authors. Everybody can submit a pull-request with a post. If you are unsure whether your post will be welcome then don't hesitate to first discuss the topic of your post on Zulip before investing too much time writing it.