Viewing profile — deadbeef57

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` b…

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

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

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://blv…

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 2 2 = 0 when you work mod 4. When you work modulo a prime, then you are working in a finite field.…

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…

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 …

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

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

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

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 …

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 …

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

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

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

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 …

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

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

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

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