Anyone up for a challenge? https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/

Quite an interesting article nonetheless.

Kevin Buzzard's opinion (https://twitter.com/XenaProject/status/1335402176332619776)

@amber_bohanna I would love to see some people working on this in Coq. I think that the HOL provers don't have a chance because I believe it will be too hard for them to handle condensed sets conveniently. But Coq, Lean, Agda and the HoTT theories have a strong enough logic.

- The Xena Project (@XenaProject)I would love to see some people working on this in Coq. I think that the HOL provers don't have a chance because I believe it will be too hard for them to handle condensed sets conveniently. But Coq, Lean, Agda and the HoTT theories have a strong enough logic.

(before everyone starts with Isabelle/HOL!)

Honestly, I don't even begin to have enough maths background to even attempt to understand the topic at hand let alone discuss whether HOL is stron enough to formalize it conveniently.

Holidays are over and Manuel still has not pushed this to the AFP? :thinking:

I'm very proud to announce that a team of Lean users has completed this challenge as of yesterday afternoon: https://leanprover-community.github.io/blog/posts/lte-final/

This is really awesome!!! By the way, I am a bit curious that roughly how many lines of Lean code have been used to complete this project.

91.000 in the project right now. I don't know how much has moved to mathlib in the mean time

91K? that is really a big project! Really looking forward to the paper.

Last updated: Dec 07 2023 at 08:19 UTC