giraj

The construction of the type 'Map<string, Type>' is entirely standard in languages like Agda and Coq (and I bet Idris too). In these languages, Type is itself a type, and can be treated like any other type (like string or int). Nothing clunky about it. (If you're curious, Type is usually referred to as a "universe type" in type theory circles.)

You're welcome! And likewise, thanks for the interesting reply.

I'm afraid I have no knowledge of your field, and no idea whether there are good tools and libraries for formalising the things you want. Maybe ask or have a look around the Proof Assistants StackExchange[1]?

There are many CS conferences through which you can publish formalised mathematics. One that comes to mind is ITP[2], but there are lots which are announced on mailing lists like TYPES-announce, coq-club, agda... You could look through previous versions of ITP and check out a few of the papers on formalising mathematics to get a feel for what these publications look like.

[1] https://proofassistants.stackexchange.com/

[2] https://mizar.uwb.edu.pl/ITP2023/

I can't speak for kxyvr, but let me chime in as a mathematician who does formalise my theorems. There's no issue with representing various foundations (e.g. ZFC) on a computer -- for example, that's essentially what Lean/mathlib does, and it's working out great for them. A "problem" with ZFC, however, is that it's very low-level, meaning there's a large distance between the "informal" proofs which mathematicians carry out and communicate, and their corresponding formal proofs in ZFC. Accordingly, for a ZFC-based mathematician to start using proof assistants, they not only have to learn how to use a proof assistant, but also to translate (or expand/elaborate) their math into ZFC.

In other foundations, such as homotopy type theory (which is what the article is about), the distance between "informal" mathematical arguments and their formal counterparts is much shorter. This is why formalisation is widespread in the HoTT-community. Indeed, I believe Voevodsky worked on HoTT in order to have a foundation which was much closer to the mathematical practice in homotopy theory.

That is an extremely uncharitable take. I find that most mathematicians care deeply that their proofs are correct.

Mechanized proofs ensure the correctness of the results they prove. That's useful. Indeed, the point of the article was that Voevodsky sought out proof assistants in order to ensure his math was correct.

As for your other questions: No, formal proofs are not intelligible to the average mathematician. They do not on their own grant insights, but the process of formalising a proof does often yield insights. (I speak from experience.) Not sure what you mean by "better"; they certainly don't replace ("informal") mathematical proofs.

You're not wrong, but most mathematicians aren't working on (or even interested in) foundations. Not saying what you mentioned isn't math (I think it is), but my point still stands.

For the math that you mention, I would suggest looking at mathlib (https://github.com/leanprover-community/mathlib). I agree that the foundations of Coq are somewhat distanced from the foundations most mathematicians are trained in. Lean/mathlib might be a bit more familiar, not sure. That said, I don't see any obstacles to developing classical real analysis or linear algebra in Coq, once you've gotten used to writing proofs in it.

I'm curious, which field of math do you work in?

Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis...

Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians.

Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.

For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:

UniMath (https://github.com/UniMath/UniMath, mentioned in the article)

Coq-HoTT (https://github.com/HoTT/Coq-HoTT)

agda-unimath (https://unimath.github.io/agda-unimath/)

cubical agda (https://github.com/agda/cubical)

All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).

Oh My Git! looks really cool and useful, thanks for mentioning it! I find it incredible that it's funded by the Prototype Fund (https://prototypefund.de/project/oh-my-git/), and it makes me wonder which other countries have similar funds hackers can apply to.

The paper argues against those who think that "programming should strive to be more mathematical" through the development and adoption of formal methods. It points out that "more mathematical" does not implicate formal methods, since proofs by mathematicians are informal and their correctness is established by social processes. The author fears that an over-emphasis on formal methods could stifle innovation (in particular, in programming language design).

As a mathematician that works with proof assistants, I largely agree with this thesis. However, I don't think there is any reason to have any such fears associated with formal methods. I think informal proofs, as the exist in both CS and maths, are here to stay. And, on the contrary, I think investigations into formal methods can drive new theory and insight. For example, one could say that the formal system of homotopy type theory (HoTT) is a programming language created in order to reason about highly "coherent" mathematical structures, which HoTT often does very well. In addition, being a formal system, HoTT is well-suited for formal methods -- but even so, many mathematicians still prefer to work informally in this language.

In summary, I think the article makes a valid point, but the motivating fears seems unfounded in retrospect.

Also "I am excited to welcome Linda Yaccarino as the new CEO of Twitter" (current front-page) is tagged 'javascript', which isn't particularly relevant.

They explain that they added an "in-app donations appeal" at the end of 2022, so I imagine that would be it.

The speed of KaTeX is great, but the lack of support for diagrams (a la tikz-cd) is what makes KaTeX unsuitable for general adoption by mathematicians (e.g., mathoverflow.net and all online mathematical wikis I know use MathJax). KaTeX has some rudimentary support for diagrams though the {CD} environment, but something more fully fledged akin to tizk-cd or xymatrix is needed. There's been some discussion on their github (https://github.com/KaTeX/KaTeX/issues/219), but I wouldn't hold my breath.

As a researcher, this sounded interesting so I had a look. The first paper that caught my eye (https://paperlist.io/post/247381561) has a bunch of "generic" (lacking substance; could be generated) comments that I find a bit uncanny. Three of them have the same style of being all lower-case (even the name of R, the programming language being discussed). Doesn't make me want to engage.

... and now I also noticed that the paper summaries are AI-generated! That's an anti-feature for me, at present.

Okay, thanks! But doesn't this still mean you have to compile ocaml (with flambda) yourself?

I updated the link to point to the docs, which are more informative. As far as I understand, flambda is an intermediate representation of OCaml which allows for a number of optimisations and better inlining. You can check if you already have flambda enabled by runnning "ocamlopt -config | grep flambda".

If you're using opam then you can test flambda out by creating a new switch

  opam switch create ocaml-flambda ocaml-variants.4.14.1+options ocaml-option-flambda

and then running "opam switch set ocaml-flambda". (You can replace 4.14.1 with your preferred version above.)

I was hoping this post would mention using OCaml with flambda[1] enabled. At least for my work, flambda seems to yield a ~10% speed up when compiling things. Can you get OCaml binaries with flambda enabled through Nix? With opam, I currently have to compile OCaml myself to enable it, as I am not aware of any binaries being distributed.

[1] https://v2.ocaml.org/manual/flambda.html

Maybe! You're certainly correct that there's a difference between knowing Lean (or a given proof assistant) vs. knowing mathlib (or some specific library). It doesn't seem to me that Codex has much of an idea about the mathlib codebase, since it e.g. invented and used "tangent_space_at_identity" out of the blue. Library-specific training would improve on this, of course.

I would reach for the usual code search tools for getting familiar with a library. For example, in Coq you have the "Search" and "Print Hint" commands which let you search for terms and instances, respectively. I imagine Lean has something similar.

This sounds like a cool demo, but I find it hard to imagine it being useful. For one, in order to check the output you need to be proficient enough that you might as well write the statement that you want. In addition, if you're working on a large library then there are small but important design decisions that matter for many statements, just like when designing ordinary software. I doubt that Codex is able to make coherent design decisions any time soon.

I would love for computers to be able to understand informal but rigorous mathematical reasoning, but, having worked with current proof assistants, it sure feels like software design will have to be solved in the same sense first.

That said, kudos for an awesome demo!

There was a thread about this roughly two weeks ago:

https://news.ycombinator.com/item?id=29349240

You're right, there's a missing step. By "a monoid M in the category C" we mean that M is an object in C along with two morphisms "unit" : 1 -> M and "multiplication" : M x M -> M satisfying the "monoid laws" translated to C. (And really C should be a so-called "monoidal category".) When C = Set, this gives the usual notion of a monoid, which classically is a set by definition, as you say. However there are lots of interesting monoid objects in other categories!

I wouldn't be surprised to see anything related to type-theory on here. And I disagree that many people doing HoTT today are proposing it as an alternative foundation in anything except (categorical) homotopy theory, and I'd like to know where you see anyone doing that.

Intuitionism in HoTT isn't about constructivity, which I agree is rejected by mainstream mathematicians. It's about the models of the theory. For example, LEM doesn't hold in the category of bundles over the circle (see my other comment on here). If you think of the axiom of choice as "every surjection has a section", then this doesn't hold for topological spaces. (Take the double cover of the circle; there's no continuous section.) I disagree that these examples are uninteresting to mainstream mathematicians.

For people wanting to learn HoTT, I'd rather recommend Rijke's book assembled from his lectures at CMU: https://github.com/EgbertRijke/HoTT-Intro

(Disclaimer: I'm a mathematician working in HoTT and (higher) category theory.)

Like with most advanced concepts in any field, there are lots of misunderstandings pertaining to HoTT. To me, the underlying insight is that the "right" abstract setting for a lot of classical homotopy theory is that of an infinity-topos (whose precise definition is an open question, but we have candidates). Theorems proven in HoTT hold in any infinity-topos, and HoTT is (conjecturally) the internal language of these.

For anything outside of homotopy theory, HoTT isn't (immediately) interesting. It's certainly not trying to provide foundations for set-based mathematics, but for (categorical) homotopy theory, sure.

Some mathematicians take issue with the logic being intuisionistic; e.g. neither the law of the excluded middle, nor double negation hold in HoTT. This is not about constructivity (which I agree, mainstream mathematicians will reject), but about the spaces being modeled. For example, a mainstream mathematician will say that a space is either empty or has a point. However, in the category of bundles over the circle, points are sections; and so the double cover doesn't have any point, for example. Neither is it empty.

Thanks for mentioning "Parsing with Zippers"! I read "Parsing with Derivatives" last week and wondered if that could be taken further. The paper can be found here: https://dl.acm.org/doi/10.1145/3408990

That's not a basis of R at all. If you want to create a basis of R you better choose irrational elements in your basis, otherwise the Q-span is contained in Q.

What I think you want to say is that "any real number has a binary expansion". Which is true, but the binary sequences don't form a vector space over R, but a Z/2-module. And as a Z/2-module, your { 2^i for integer i } isn't even a basis because you need infinite expansions to express most real numbers. The span of a basis are only the finite linear combinations.

(FWIW, I think you've given a description of the dyadic rationals.)

You're right, any basis of R over Q has to be uncountably infinite. If a countable basis existed, we could for example write R as the union of the subspaces spanned by the n first basis elements, indexed by n. That would mean R is countable, since a countably-indexed union is countable.

My work is related to homotopy type theory. There are mathematicians working in Agda and Lean (2, but also 3) as well, but it certainly is a niche field.

Could you elaborate or illustrate what you mean by "theorem proving systems that embrace the full spectrum of abstract and correct thought"?

As a mathematician (and programmer on the side) who regularly works in Coq, my impression is that Rust does represent "the future of programming" (or rather, my ideal of it). Type systems are the only mechanism (that I know of) for formally ensuring properties of programs, and proof assistants and languages like Rust lie on two extremes of the spectrum. The former puts the type system in focus; indeed all my work in Coq is about convincing the compiler that certain functions (terms) type-check. The latter puts types in the background, trying to prove as much as possible with minimal friction.

What's the alternative?

You've clearly thought about this, and certainly begrudging use is better than none. My first thought would have been to go with Signal, if GChat through your school doesn't work. I've had no issues with group chats on there.

"Perfect is the enemy of good" -- you're making the right decision by focusing on good mentorship offering instead of blocking on the perfect chat solution. Good luck!