I recently learned about some limitations in both Coq and Lean theorem prover after watching the video by Kevin Buzzard on formalization of math in Lean. He did

I recently learned about some limitations in both Coq and Lean theorem prover after watching the video by Kevin Buzzard on formalization of math in Lean. He did some claims about quotient support in Coq, so I just asked[1] Coq developers straightly. I recommend to read their discussion and explanations. [1] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871