deadbeef57

3 年前議論

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

deadbeef57

3 年前議論

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! Look at the papers about hygienic macros, or functional-but-in-place, or any of the others.

deadbeef57

3 年前議論

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). Unfortunately there is not yet a fancy graph showing the growth of mathlib4.

deadbeef57

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?

deadbeef57

4 年前議論

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 user group)

deadbeef57

4 年前議論

2 times 2 = 0 mod 4. Sorry for the markdown mess-up.

deadbeef57

4 年前議論

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 elements is not* the same as working mod 4. Finite fields of size p^n are not the same as (not isomorphic to!) the ring Z/(p^nZ) whenever n > 1.

Just because there exists a finite field of size 2^n doesn't mean that any length-n-bit-string that is the output of a hash function lives in a finite field of size 2^n.

Adding and multiplying hashes doesn't make any sense. If it does then you have a very weird hash function. Not one of the standard cryptographic hashes. So saying that a hash function maps onto a finite field sounds pretty confused to me.

deadbeef57

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 with the interactive theorem prover behind it: Lean [2]. There's also plenty other interactive theorem provers (Coq, Isabelle, HOL, Mizar, Metamath, ...) but Lean has a lot of traction amongst mathematicians at the moment.

There are no limits to the math you an do with this. There is mathlib [3], the main mathematical library. It covers a lot of undergraduate material [4], and plenty of stuff beyond that [5]. The community has even covered some state of the art research math in Lean [6a, 6b].

You are very welcome to hang out on the leanprover zulip [7]] and ask questions about the Natural Number Game or anything else that is Lean-related.

[1]: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... [2]: https://leanprover-community.github.io/ [3]: https://github.com/leanprover-community/mathlib [4]: https://leanprover-community.github.io/undergrad.html [5]: https://leanprover-community.github.io/mathlib-overview.html [6a]: https://github.com/leanprover-community/lean-liquid [6b]: https://www.nature.com/articles/d41586-021-01627-2 [7]: https://leanprover.zulipchat.com/

deadbeef57

4 年前議論

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 roughly the same.

deadbeef57

4 年前議論

> 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. Don't spend years not finding the perfect person. Find a good person on the same wavelength, get on the job.

To raise kids (in a responsible good manner), you need a long-lasting stable relationship with parents that are trustworthy and on the same wavelength.

OP is currently in a relationship with his wife whom he loves dearly. But regarding kids they don't seem to be on the same wavelength (on one particular topic, they probably agree on many other things), because he regrets decisions they made in the past.

Why will his situation improve by giving up the relationship and becoming less trustworthy? 5 years down the roads, in a new relationship, he or his new wife will decide their wavelengths changed, and it's time to look for someone else. And then 2 small kids will have to cope with the fall-out.

Divorcing someone you love, with the intents of starting a stable relationship with someone else is self-deceit. Kids deserve better than that.

deadbeef57

4 年前議論

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 recognize. And that's not where you find happiness and a fulfilling life.

(Aside: your attempt to make the suggestion colorful by adding that the woman should be religious is quite weird. For many religious people, selfishness and divorce are not things that make a partner attractive.)

deadbeef57

4 年前議論

my first thought was: why not move to Zulip in general?

deadbeef57

4 年前議論

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 unfunny joke without providing any serious reason.

deadbeef57

4 年前議論

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 certain thread, and then it only used < 50% of my screen to show the conversation.

Zulip > Slack, even without this new change that Slack is dumping on users.

deadbeef57

4 年前議論

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)
  - categorytheory.zulipchat.com (~600 messages / week)

as well as the quieter

  - isabelle.zulipchat.com
  - hott.zulipchat.com

For research groups, it seems to work exceedingly well. The UI is unobtrusive, and values my screen real estate. (Slack only devotes < 50% of the screen to the actual conversation. On Zulip, the list of users and threads are delegated to the margins, so that the actual messages have the center stage.)

Besides that, I find that Zulip found the Goldilocks-equilibrium with its threading model. It works really well for both synchronous and asynchronous conversations, and you can easily switch back and forth between the two within one thread.

I'm a big fan.

deadbeef57

4 年前議論

(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 operations are smooth. -/
  -- See note [Design choices about smooth algebraic structures]
  @[ancestor has_smooth_mul, to_additive]
  class lie_group {𝕜 : Type*} [nontrivially_normed_field 𝕜]
    {H : Type*} [topological_space H]
    {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H)
    (G : Type*) [group G] [topological_space G] [charted_space H G]
    extends has_smooth_mul I G : Prop :=
  (smooth_inv : smooth I I (λ a:G, a⁻¹))

In particular, the output of Lean Chat didn't talk at all about needing a smooth inverse function.

Anyway, I very much agree with you that there are risks here. At the same time, I think this can be an extremely useful tool for new users trying to get started. Because mathlib is approaching 1M lines of code, and a tool like this might help a lot in discovering parts of the library. As you say, it can already be used as some sort of snippet-engine-on-steroids.

deadbeef57

4 年前議論

That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.

deadbeef57

4 年前議論

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. But since 99.9% of mathematicians have never heard of constructive mathematics, and just use AoC or LEM all over the place, I am quite certain that Gowers is very much interested in how to find proofs in the "ordinary" sense: including the use of AoC and LEM.

deadbeef57

4 年前議論

> 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 less what Gowers is after. And that's exactly why he wants GOFAI instead of ML. He wants to understand how "doing mathematics" works?

deadbeef57

4 年前議論

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?

コメント