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

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.

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.

I believe @Patrick Nicodemus is aware of this

but we're talking about math-comp though

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

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