Julian (Dec 06 2020 at 13:07): Julian (Dec 06 2020 at 13:07):Anyone up for a challenge? https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/
Quite an interesting article nonetheless.
Mathias Fleury (Dec 06 2020 at 13:26):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.
Mathias Fleury (Dec 06 2020 at 13:28):(before everyone starts with Isabelle/HOL!)
Julian (Dec 06 2020 at 14:24):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.
Simon Wimmer (Jan 06 2021 at 14:28):Holidays are over and Manuel still has not pushed this to the AFP? :thinking:
Johan Commelin (Jul 15 2022 at 22:04):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/
Wenda Li (Jul 16 2022 at 03:09):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.
Johan Commelin (Jul 16 2022 at 07:28):91.000 in the project right now. I don't know how much has moved to mathlib in the mean time
Wenda Li (Jul 16 2022 at 07:34):91K? that is really a big project! Really looking forward to the paper.
Last updated: Dec 21 2024 at 12:33 UTC