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...
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?
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.
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.
>> 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.
Well it would be ideal but lots of kids have separated parents.
What is important is not that the parents are together, but that everyone is safe, the kids are loved, the parents are respectful towards one another. The greater the kindness and cooperation between separated parents, the better it is for kids.
Critically important is that the kids are not exposed to conflict between parents.
If you can get all that right then even kids with separated parents can be pretty happy I think.
However harmonious the relationship following the split, it’s still damaging for children in that situation.
It may be increasingly common and I’d agree it’s better to separate than stay together for the kids but I do believe it has a lasting impact. It’ll affect the way they see relationships for the rest of their lives.
It’s selfish for people in their late 30s / early 40s to rush into having a family because they’re worried the window will close.
> you need a long-lasting stable relationship with parents that are trustworthy and on the same wavelength.
Also this is an extremely western centric mindset. iirc the literature indicates that having 2 responsible well caring adults is a much better goal. That could simply be an Uncle and Grandma. If OP has a community/network of good people then it's ok if He/Wifey are not perfect.
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.)
