giraj

6 ms·

1.
Open Letter to the European Commission(nixos.org)
60 points by giraj 2y ago|26 comments
2.
by giraj 2y ago
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 in
3.
BB(5) = 47,176,870(discuss.bbchallenge.org)
5 points by giraj 2y ago|1 comments
4.
by giraj 3y ago
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 aro
5.
by giraj 3y ago
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&#x2F
6.
by giraj 3y ago
That is an extremely uncharitable take. I find that most mathematicians care deeply that their proofs are correct.
7.
by giraj 3y ago
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
8.
by giraj 3y ago
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.
9.
by giraj 3y ago
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 a
10.
by giraj 3y ago
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 formalisatio
11.
by giraj 3y ago
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) C
12.
by giraj 3y ago
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
13.
by giraj 3y ago
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 m
14.
by giraj 3y ago
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.
15.
by giraj 3y ago
They explain that they added an "in-app donations appeal" at the end of 2022, so I imagine that would be it.
16.
by giraj 3y ago
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
17.
by giraj 3y ago
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 th
18.
by giraj 4y ago
Okay, thanks! But doesn't this still mean you have to compile ocaml (with flambda) yourself?
19.
by giraj 4y ago
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 hav
20.
by giraj 4y ago
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 currentl
21.
by giraj 4y ago
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 mathli
22.
by giraj 4y ago
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 workin
23.
by giraj 5y ago
There was a thread about this roughly two weeks ago: https://news.ycombinator.com/item?id=29349240
24.
by giraj 5y ago
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
25.
by giraj 6y ago
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
26.
by giraj 6y ago
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 (hig
27.
by giraj 6y ago
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&#x2F
28.
by giraj 6y ago
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 exp
29.
by giraj 6y ago
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 coun
30.
by giraj 6y ago
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.

More ›