metiulekm

@metiulekm@sh.itjust.works

• ⁨Comment⁩ on ⁨Are LLMs capable of writing *good* code?⁩ ⁨⁨3⁩ ⁨months⁩ ago⁩:

  Hasn’t Google already made advances through its Alpha Geometry AI?? Admittedly, that’s a geometry setting which may be easier to code than other parts of Math and there isn’t yet a clear indication AI will ever be able to reach a certain level of creativity that the human mind has, but at the same time it might get there by sheer volume of attempts.

  Wanted to focus a bit on this. The thing with AlphaGeometry and AlphaProof is that they really treat doing math as a game, not unlike chess. For example, AlphaGeometry has a basic set of rules, it can apply them and it knows when it is done. And when it is done, you can be 100% sure that the solution is correct, because the rules of the game are known; the 28/42 score reported in the article is really four perfect scores and three zeros. Those systems do use LLMs, but they really are only there to suggest to the system what to try doing next. There is a very enlightening picture in the AlphaGeometry paper here: www.nature.com/articles/s41586-023-06747-5#Fig1

  You can automatically verify correctness of code the same way. For example Lean, the language AlphaProof uses internally, can be used for general programming. In general, we call similar programming techniques formal methods. But most people don’t do this, since this is more time-consuming than normal programming, and in many cases we don’t even know how to define the goal of our code (how to define correct rendering in a game?). So this is only really done when the correctness of the program is critical, like famously they verified the code of the automatic metro in Paris this way. And so most people don’t try to make programming AI work this way.

• ⁨Comment⁩ on ⁨Dark Souls would’ve been a better game in early access, says dev behind Dark Souls-like early access game No Rest For The Wicked⁩ ⁨⁨7⁩ ⁨months⁩ ago⁩:

  I can personally say that I got super excited by the new release from the Ori devs at first, though later became disinterested because the game is so different. The Ori games weren’t obscure by any means, so I am not surprised other people got excited too.

• ⁨Comment⁩ on ⁨What are the most mindblowing fact in mathematics?⁩ ⁨⁨1⁩ ⁨year⁩ ago⁩:

  It seems that I can’t see the link from 0.18.3 instances somehow. Maybe one of these will work: math.stackexchange.com/a/18347 https://math.stackexchange.com/a/18347 https://math.stackexchange.com/a/18347

• ⁨Comment⁩ on ⁨What are the most mindblowing fact in mathematics?⁩ ⁨⁨1⁩ ⁨year⁩ ago⁩:

  Imagine a soccer ball. The most traditional design consists of white hexagons and black pentagons. If you count them, you will find that there are 12 pentagons and 20 hexagons.

  Now imagine you tried to cover the entire Earth in the same way, using similar size hexagons and pentagons (hopefully the rules are intuitive). How many pentagons would be there? Intuitively, you would think that the number of both shapes would be similar, just like on the soccer ball. So, there would be a lot of hexagons and a lot of pentagons. But actually, along with many hexagons, you would still have exactly 12 pentagons, not one less, not one more. This comes from the Euler’s formula, and there is a nice sketch of the proof here: math.stackexchange.com/a/18347.

• ⁨Comment⁩ on ⁨What are the most mindblowing fact in mathematics?⁩ ⁨⁨1⁩ ⁨year⁩ ago⁩:

  Every prime larger than 3 is either of form 6k+1, or 6k+5; the other four possibilities are either divisible by 2 or by 3 (or by both). Now (6k+1)² − 1 = 6k(6k+2) = 12k(3k+1) and at least one of k and 3k+1 must be even. Also (6k+5)² − 1 = (6k+4)(6k+6) = 12(3k+2)(k+1) and at least one of 3k+2 and k+1 must be even.

• ⁨Comment⁩ on ⁨Wikihow brutally kills 36 year olds⁩ ⁨⁨1⁩ ⁨year⁩ ago⁩:

  Honestly I’ve unironically missed the entirety of the image at first, I went directly to the text. And probably a lot of internet-savvy people would, this kind of image is useless decoration 90% of the time and people are trained to not look at it. Same concept as in that research where they asked people to find the current population number on a webpage and they had a very hard time, despite the value being in big red digits or something equally distinctive.