deadbeef57

8 ms·

1.
by deadbeef57 3y ago
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...
2.
by deadbeef57 4y ago
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 lan
3.
by deadbeef57 4y ago
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 version of mathlib).
4.
by deadbeef57 4y ago
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?
5.
by deadbeef57 4y ago
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 l
6.
by deadbeef57 4y ago
2 times 2 = 0 mod 4. Sorry for the markdown mess-up.
7.
by deadbeef57 4y ago
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. Working in the finite field of 4 elements is not* the
8.
by deadbeef57 4y ago
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 wi
9.
by deadbeef57 4y ago
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" so
10.
by deadbeef57 4y ago
> 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 same boat as you
11.
by deadbeef57 4y ago
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 behavior, as you
12.
by deadbeef57 4y ago
my first thought was: why not move to Zulip in general?
13.
by deadbeef57 4y ago
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 unfu
14.
by deadbeef57 4y ago
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 certa
15.
by deadbeef57 4y ago
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 / w
16.
by deadbeef57 4y ago
(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 inverse
17.
by deadbeef57 4y ago
That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
18.
by deadbeef57 4y ago
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 constructively. Bu
19.
by deadbeef57 4y ago
> 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. This is more or
20.
by deadbeef57 4y ago
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 yea
21.
by deadbeef57 5y ago
There are a lot of problems with that article. See https://news.ycombinator.com/item?id=8797002 for a discussion.
22.
by deadbeef57 5y ago
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.
23.
by deadbeef57 5y ago
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 computer. Conversely
24.
by deadbeef57 5y ago
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 hand &
25.
by deadbeef57 5y ago
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 talking specifi
26.
by deadbeef57 5y ago
I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical. It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read
27.
by deadbeef57 5y ago
In my experience, the difficulty is very rarely the transition from set theory to type theory. I find this almost transparent in practice. The issue is rather that you need to deal with edge cases that are usually swept under the rug, or th
28.
by deadbeef57 5y ago
Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.
29.
by deadbeef57 5y ago
Sure, I just created an account a couple of days ago, and my favourite username was already taken :oops: I'm Johan Commelin, https://math.commelin.net/
30.
by deadbeef57 5y ago
You might enjoy http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game... It's a game implemented in lean, where you work your way through the basic facts about natural numbers.

More ›