No, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode. Examples: `\times` becomes `×` and `\to` becomes `→`, etc...
Please take a look at the papers about Lean (https://leanprover-community.github.io/papers.html) and explain to me how that "reinvents everything". There are several new and non-trivial things going on in this language!…
Note that the sudden drop-off at the end of the graph that shows commits-per-month is because this is measuring commits-to-mathlib3. A lot of contributors are currently helping with the port-to-mathlib4 (aka the Lean 4…
Isn't the whole US constitution a collection of human-made sentences? Who cares if some one tacks on extra "forged" sentences? What does forged even mean in this context?
I don't have a specific programming recommendation. But I know there are several blind programming wizards. Maybe these links are helpful? - https://the-brannons.com/ - https://blvuug.org/ (blind and low-vision unix…
2 times 2 = 0 mod 4. Sorry for the markdown mess-up.
That's flat out wrong. Working modulo 4 is not working in a finite field, because 22 = 0 when you work mod 4. When you work modulo a prime, then you are working in a finite field. Working in the finite field of 4…
Take a look at the Natural Number Game! [1] It does exactly that: "Rapid feedback, error messages, maybe even linters and highlighting for the "mathematical syntax"." After you get the hang of the system, you can play…
Is it really clear that GPT does not "know" the letters that compose a token? It is pretty amazing at poetry and rhyming. Probably it is able to infer from all this knowledge that "in ten did" and "intended" sound/spell…
> Choose a good and kind trustworthy woman who you think would be a good mother. Make sure you bring the same things to the party. You don't need a perfect relationship. There are many women out there in exactly the…
I think this is very very bad advice. You don't fix one mistake by making another one. OP said that he dearly loves his wife. I think that's marvelous and he should treasure that. Divorce would indeed be selfish…
my first thought was: why not move to Zulip in general?
I'm a huge fan of Zulip. I use it heavily on leanprover.zulipchat.com (~4000 messages/week). I've never used it in the setting of a company. What kind of issues did you hit? Doesn't sound fair to me to call Zulip an…
Zulip didn't just "copy [Slack] exactly". The UX is much better than Slack, in my opinion. It's faster, and it puts the conversations center stage. With Slack I always felt that I had too click too much to get to a…
Big fan of Zulip here. Admittedly, I haven't used Zulip in the context of a company. But I'm a happy user of - leanprover.zulipchat.com (~4000 messages / week) - coq.zulipchat.com (~1200 messages / week) -…
(I'm the Johan Commelin mentioned in the blogpost.) In fact, `lie_group` exists in mathlib, and is defined as follows: /-- A Lie group is a group and a smooth manifold at the same time in which the multiplication and…
That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
Here's my guess. Gowers wants to understand how the typical mathematician comes up with a proof. How is the proof found? Where do the ideas come from? To some extent, this is orthogonal to whether or not you do maths…
> And vice versa. For it to do so, it has to be better than the human, also have a model of how the human thinks, and then be able to break down thinking it arrived at one way to something that makes sense to the human.…
Such an "AlphaZero approach" will only knock Gowers's GOFAI approach out of business if the AI can also "justify" its proofs, in the sense that Gowers explains in his blogpost. Do you think that will happen in 5 years?
There are a lot of problems with that article. See https://news.ycombinator.com/item?id=8797002 for a discussion.
You still need to check that the definitions are correct. If you define `x^n = 42`, then proving FLT for `n > 2` is really easy. And proof checkers cannot check that you get the definitions right.
Homotopy type theory (HoTT) can mean several things: it's a new foundation of mathematics that was developed from the start with computer-formalization in mind. But you can also work on HoTT without ever touching a…
I just want to say that in the case of the classification of finite simple groups, there's actually a bit of a problem. Exactly because "a lot of the deep expertise mathematicians" have left the field; but on the other…
Right now, I think I would go for that classical approach, simply because there is more supporting material for that in the library, and there are more people who understand that approach and can help contributing. (I'm…
No, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode. Examples: `\times` becomes `×` and `\to` becomes `→`, etc...
Please take a look at the papers about Lean (https://leanprover-community.github.io/papers.html) and explain to me how that "reinvents everything". There are several new and non-trivial things going on in this language!…
Note that the sudden drop-off at the end of the graph that shows commits-per-month is because this is measuring commits-to-mathlib3. A lot of contributors are currently helping with the port-to-mathlib4 (aka the Lean 4…
Isn't the whole US constitution a collection of human-made sentences? Who cares if some one tacks on extra "forged" sentences? What does forged even mean in this context?
I don't have a specific programming recommendation. But I know there are several blind programming wizards. Maybe these links are helpful? - https://the-brannons.com/ - https://blvuug.org/ (blind and low-vision unix…
2 times 2 = 0 mod 4. Sorry for the markdown mess-up.
That's flat out wrong. Working modulo 4 is not working in a finite field, because 22 = 0 when you work mod 4. When you work modulo a prime, then you are working in a finite field. Working in the finite field of 4…
Take a look at the Natural Number Game! [1] It does exactly that: "Rapid feedback, error messages, maybe even linters and highlighting for the "mathematical syntax"." After you get the hang of the system, you can play…
Is it really clear that GPT does not "know" the letters that compose a token? It is pretty amazing at poetry and rhyming. Probably it is able to infer from all this knowledge that "in ten did" and "intended" sound/spell…
> Choose a good and kind trustworthy woman who you think would be a good mother. Make sure you bring the same things to the party. You don't need a perfect relationship. There are many women out there in exactly the…
I think this is very very bad advice. You don't fix one mistake by making another one. OP said that he dearly loves his wife. I think that's marvelous and he should treasure that. Divorce would indeed be selfish…
my first thought was: why not move to Zulip in general?
I'm a huge fan of Zulip. I use it heavily on leanprover.zulipchat.com (~4000 messages/week). I've never used it in the setting of a company. What kind of issues did you hit? Doesn't sound fair to me to call Zulip an…
Zulip didn't just "copy [Slack] exactly". The UX is much better than Slack, in my opinion. It's faster, and it puts the conversations center stage. With Slack I always felt that I had too click too much to get to a…
Big fan of Zulip here. Admittedly, I haven't used Zulip in the context of a company. But I'm a happy user of - leanprover.zulipchat.com (~4000 messages / week) - coq.zulipchat.com (~1200 messages / week) -…
(I'm the Johan Commelin mentioned in the blogpost.) In fact, `lie_group` exists in mathlib, and is defined as follows: /-- A Lie group is a group and a smooth manifold at the same time in which the multiplication and…
That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
Here's my guess. Gowers wants to understand how the typical mathematician comes up with a proof. How is the proof found? Where do the ideas come from? To some extent, this is orthogonal to whether or not you do maths…
> And vice versa. For it to do so, it has to be better than the human, also have a model of how the human thinks, and then be able to break down thinking it arrived at one way to something that makes sense to the human.…
Such an "AlphaZero approach" will only knock Gowers's GOFAI approach out of business if the AI can also "justify" its proofs, in the sense that Gowers explains in his blogpost. Do you think that will happen in 5 years?
There are a lot of problems with that article. See https://news.ycombinator.com/item?id=8797002 for a discussion.
You still need to check that the definitions are correct. If you define `x^n = 42`, then proving FLT for `n > 2` is really easy. And proof checkers cannot check that you get the definitions right.
Homotopy type theory (HoTT) can mean several things: it's a new foundation of mathematics that was developed from the start with computer-formalization in mind. But you can also work on HoTT without ever touching a…
I just want to say that in the case of the classification of finite simple groups, there's actually a bit of a problem. Exactly because "a lot of the deep expertise mathematicians" have left the field; but on the other…
Right now, I think I would go for that classical approach, simply because there is more supporting material for that in the library, and there are more people who understand that approach and can help contributing. (I'm…