Se ha publicado un nuevo proyecto de formalización en Lean 4 basado en el libro Calculus de Spivak. Este proyecto, desarrollado por Jon-Erik G. Storm en colaboración con Claude, se encuentra en el repositorio SpivakCalculus de GitHub.