Stream: math-comp users

Topic: Terence Tao is trying out Lean


view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:14):

Hi folks, this may be of interest to some, Terence Tao is playing with mathlib; I wonder how he'd fare with math-comp?

Details are at https://mathstodon.xyz/@tao

view this post on Zulip Patrick Nicodemus (Oct 20 2023 at 23:13):

I was unable to ever really get the hang of math-comp. SSReflect is great but math-comp just has a lot of design patterns that are hard to understand. Honestly I wouldn't recommend it to a friend who wasn't familiar with Coq because I think would be overwhelming. It is difficult to write a proof in the math-comp library armed with just understanding of Coq alone.

view this post on Zulip grianneau (Oct 21 2023 at 06:38):

Patrick Nicodemus said:

I was unable to ever really get the hang of math-comp. SSReflect is great but math-comp just has a lot of design patterns that are hard to understand. Honestly I wouldn't recommend it to a friend who wasn't familiar with Coq because I think would be overwhelming. It is difficult to write a proof in the math-comp library armed with just understanding of Coq alone.

SSReflect is part of Coq. One can just use the tactics from SSReflect without math-comp.

view this post on Zulip Huỳnh Trần Khanh (Oct 21 2023 at 06:48):

I believe @Patrick Nicodemus is aware of this

view this post on Zulip Huỳnh Trần Khanh (Oct 21 2023 at 06:49):

but we're talking about math-comp though

view this post on Zulip grianneau (Oct 21 2023 at 07:21):

The message is also about SSReflect and it would be sad to put off users.

view this post on Zulip Pierre Roux (Oct 21 2023 at 07:36):

Also note that mathcomp is probably not much different from mathlib in that one has to first learn before efficiently using it. The mathcomp book helps a lot IMHO https://math-comp.github.io/mcb/


Last updated: Jul 25 2024 at 14:01 UTC