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

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.

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

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

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/

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.

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

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

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

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.

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.

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

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

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

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

Conversely, there are many ways to do computer-formalization of mathematics, without every doing anything with HoTT.

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 "a small, curated subset of these techniques" is still missing. A small group of experts (all in their 70's or 80's) are currently writing a dozen volumes on this classification, and the rest of the community hopes that they get it done before they pass away.

This proof has a seriously low bus factor at the moment :scared:

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 specifically about functional analysis and PDEs here.)

On the other hand, it should be a lot of fun to see if we can formalize the new proof by Clausen--Scholze of Serre duality. Using their machinery, the proof should simplify a lot. But this requires building complex analytic manifolds on top of condensed mathematics. So we would first need to set up those foundations.

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 every part of Lean's documentation or website. I might be missing something obvious here.)

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 that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these tedious parts of formalization, and I'm very glad that people are working hard on realizing this.

Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.

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/

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.