Stream: General

Topic: Liquid tensor experiment


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Dec 06 2020 at 13:28):

(before everyone starts with Isabelle/HOL!)

view this post on Zulip 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.

view this post on Zulip Simon Wimmer (Jan 06 2021 at 14:28):

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

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Wenda Li (Jul 16 2022 at 07:34):

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


Last updated: Aug 15 2022 at 02:13 UTC