Viewing profile — giraj

The construction of the type 'Map ' 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 an…

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…

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 -- f…

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 ensur…

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 fr…

Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reason…

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/UniMa…

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 …

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 m…

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 a…

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; c…

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 optimis…

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 bina…

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 th…

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…

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 …

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 e…