giraj

hace 2 añosdiscuss

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.)

giraj

hace 3 añosdiscuss

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/

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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...

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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).

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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.

giraj

hace 3 añosdiscuss

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

giraj

hace 3 añosdiscuss

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.)

giraj

hace 3 añosdiscuss

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

giraj

hace 4 añosdiscuss

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.

giraj

hace 4 añosdiscuss

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!

Submissions

Open Letter to the European Commission

BB(5) = 47,176,870

Show HN: Melatonin for Chrome – automatic color temperature for chromebook users

comments