I'm not a mathematician, but how credible is that anti-Lean material? Are they marketing an alternative programmatic approach, as in they're anti-lean because "I got something else" or are they philosophically anti-Lean and have valid arguments?
'Vibe formalizing' is a logical extension of 'vibe engineering' implemented by 'vibe coding'. Sometimes I have trouble with getting the individual puzzle pieces of a problem to fall into place, where a hypothetical 'Move 37 As A Service' to unify informal methods with mathematical rigor deserves to be explored!
I had put on the back burner some polyhedral compilation papers. I had read all the material, but some key questions still meant it was not possible for me to implement it. In particular, I was looking at barvinoks counting algorithm and did not understand why you needed to expand the polynomials in a pointed cone. However, chatgpt correctly led me through the reasoning. Could it have made a mistake? Of course. And it did. However, since my confusion meant that I was also wrong, bouncing the idea back and forth was really useful. Plus the ai bots are better at understanding your own particular points of confusion.
Having the ability to throw math heavy ML papers at the assistants and get simplified explanations / pseudocode back is absolutely amazing, as someone who's forgot most of what I learned in uni, 25+ years back and never really used it since.
I've had mixed results with AI on research mathematics. I've gotten it to auto-complete non-trivial arguments, and I've found some domains where it seems hopelessly lost. I think we're still at a point in history where mathematicians will not be replaced by AI and can only benefit by dabbling with it.
I was told by a hungarian, that hungarian written spelling and spoken pronunciation is pretty precisely aligned compared to, say, english. Except when it comes to names when it gets a bit random!
Why not do the bloke the decency to spell his name correctly? Those diacritics are important.
Anyway, I was told that Paul's name is very roughly pronounced by an anglophone as: "airdish".
I take it that that's a palatalized ending? I read your comment at first and was like "airdish" wtf? Then I palatalized the 'os' ending and realized oh yeah... that does sound kind of like airdish!
Ő is just œ (oe), nothing crazy. Certainly not a scenario that would belong to the quirky category.
The only weird ones I can think of are the ones that end in -y. For example, Görgey. They're meant to be -i endings. They signify a noble lineage (or at least used to).
I guess "ch" might also show up every now and then too (it's just "cs", just like "ch" in English). For example, Széchényi.
Since this is a compsci forum to some extent, maybe I should also mention that the so-called Lanczos-interpolation is "actually" Lánczos. Took even me a while to pick up on that one! Thinking about it, I now see that it features a "cz", another letter (digraph) that is longer part of the alphabet.
Also note that Paul is a "translated" name. His actual name was Pál Erdős. He got lucky with that one, it's an easy swap. Edward Teller (Ede Teller) was the same way, and so was John (von) Neumann (János Neumann).
As a bonus trivia, the Hungarian name order is big endian, like the Japanese. So it would be "Erdős Pál", "Teller Ede", "Neumann János", and "Lánczos Kornél". Though just like with Japanese, I would not recommend trying to adhere to this order in most English speaking contexts.
The "weird" part about Hungarian names and words for English speakers is that "y" is a modifier letter in most cases, not a sound in and of itself. So e.g. "Nagy" is pronounced closer to something like "Nahj".
I was driving around tonight doing errands and while I was doing so, had a great conversation with chatgpt as to the intimate details of the llvm and GCC pipeline schedulers. It's a huge productivity boost. It has now taken notes for me for some compiler stuff I'm experimenting with. This would previously have been impossible.
I still can't believe that we are in the era of 'star trek' like "Computer plot me a proof for this math problem" in my life time! Wish we could also do the same for "Beam me up scotty"
18 comments
[ 2.7 ms ] story [ 43.6 ms ] threadEven imperfect assistants increase leverage.
I was told by a hungarian, that hungarian written spelling and spoken pronunciation is pretty precisely aligned compared to, say, english. Except when it comes to names when it gets a bit random!
Why not do the bloke the decency to spell his name correctly? Those diacritics are important.
Anyway, I was told that Paul's name is very roughly pronounced by an anglophone as: "airdish".
The only weird ones I can think of are the ones that end in -y. For example, Görgey. They're meant to be -i endings. They signify a noble lineage (or at least used to).
I guess "ch" might also show up every now and then too (it's just "cs", just like "ch" in English). For example, Széchényi.
Since this is a compsci forum to some extent, maybe I should also mention that the so-called Lanczos-interpolation is "actually" Lánczos. Took even me a while to pick up on that one! Thinking about it, I now see that it features a "cz", another letter (digraph) that is longer part of the alphabet.
Also note that Paul is a "translated" name. His actual name was Pál Erdős. He got lucky with that one, it's an easy swap. Edward Teller (Ede Teller) was the same way, and so was John (von) Neumann (János Neumann).
As a bonus trivia, the Hungarian name order is big endian, like the Japanese. So it would be "Erdős Pál", "Teller Ede", "Neumann János", and "Lánczos Kornél". Though just like with Japanese, I would not recommend trying to adhere to this order in most English speaking contexts.