Ramkumar Ramachandra

I've self-taught myself undergraduate-level Mathematics, and am currently enrolled in an advanced Masters program specialized in higher category theory at Université de Paris. Here are some thoughts: First, the amount I learnt on a day-to-day basis from self-studying in my free time pales in comparison to the amount I learnt from a structured course ending with an exam, in which you have to commit to studying 2~4 hours of math every single day. Second, classroom lectures mainly act as a structured table-of-contents for working through various textbooks. The problem sheets they distribute in the tutorials are very helpful, as is the discussion of problems that some students might have got stuck in. Graduate-level math textbooks are fantastic, and the authors have poured 10+ years of their lives writing them. No online course with cute interactive video can substitute them. Having said that, there are some video lectures that can act as good motivation for studying a subject. For instance, Wildberger's lectures on algebraic topology (find them on YouTube) are a great starting point for the subject. You first have to decide on what you want to learn, by looking through various fields, and narrow your scope. Mathematics is a huge discipline, and you have to decide what you like, and work through the prerequisites in a disciplined manner. I cannot emphasize the importance of working through exercises enough. All mathematics textbooks have exercises at the end of each…

Lean is a great idea, especially the 4th version, a huge level up from the 3rd one, but its core still deficient[1] in some particular scenarious (see an interesting discussion[2] in the Rock (formerly Coq) issue tracker). Not sure if it might hinder the automation with the AI. [1] https://artagnon.com/logic/leancoq [2] https://github.com/rocq-prover/rocq/issues/10871

I am still very new to proof theory. So please take this with a mountain of salt. At the core all these proof assistants, is a dependent total functional programming language. Total means all functions must be obviously be terminating. Dependent means types can dependent on values or more generally you can have quantifiers (sigma and pi). Both Coq and Lean have variants of a dependent type theory called “Calculus of Inductive Constructions”. Coq and Lean have tactics which can be thought of an embedded “proof language”. It’s an useful fiction because underneath it is just functions and inductive definitions. Agda and Idris doesn’t have tactics, so the proofs have to be done through computation (by defining and apply functions and data types) Lean and Coq differ in how they encode mathematical objects. Lean makes it much easier to make use of classical axioms. (Defining axioms is easy in both Lean and Coq) From a more practical POV, Coq has the best documentation, books and development tools. Lean has the WORST development tools of all 4. However has extensive libraries for mathematics. ( It is very painful to use ) Agda and Idris are about the same (set up is a pain otherwise about as good as Haskell development) Even though Idris is marketed for “practical programming” it doesn’t have partial functions!! I am not sure if Agda supports partial functions. A more thorough comparison can be found here : https://artagnon.com/articles/leancoq

probably chinese https://artagnon.com/art/xi