Successful completion of the Liquid Tensor Experiment, a challenge posed to the Lean prover community by Peter Scholze, after a year and a half of effort:

...where here "completion" appears to mean that the initial goal has been attained, but the associated repo still seems to be under active development. And apparently they are in dependency hell with mathlib:

· · Web · 0 · 1 · 1
Sign in to participate in the conversation

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!