I have gone down this road and tried to use Jira, Trello, etc for project tracking for things other than my job, including hobby dev projects. After decades, I landed on text files in outline form (markdown sometimes for things like design docs). Way less clicks and page loads, way easier to back up, completely not dependent on proprietary/closed-source behaviors. I use them to take meeting notes, plan my projects, track deliverables/action items, jot down ideas for videos I want to make and mod ideas for games I play. Very effective.
I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?
I can't find a link to an actual paper, that just seems to be a blog post. But from what I gather the problems were manually translated to Lean 4, and then the program is doing some kind of tree search. I'm assuming they are leveraging the proof checker to provide feedback to the model.
Yeah, as a former research mathematician, I think “fumbling around blindly” is not an entirely unfair description of the research process.
I believe even Wiles in a documentary described his search for the proof of Fermat’s last theorem as groping around in a pitch black room, but once the proof was discovered it was like someone turned the lights on.
They just write "it's like alpha zero". So presumably they used a version of MCTS where each terminal node is scored by LEAN as either correct or incorrect.
Then they can train a network to evaluate intermediate positions (score network) and one to suggest things to try next (policy network).
The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found.
So they had three days to keep training the model, on synthetic variations of each IMO problem.
Just my anecdotal two cents: what you're saying simply does not match my life experience. The model bit is debatable, but the predicted outcomes are demonstrably false for me and a lot of people I know.
Yes this system produces “wins” and it’s generally at someone’s expense. There are exceptions of course, like everything but this is the general distribution
The whole point though is that if you’re a winner in the game has very little to do with being or having a “good” manager
I was always fascinated by stuff like LSB stenography where you hide a message (or another image) in the least significant bits of an image. Not visible to the human eye, mathematically should look like thermal noise in the image at most.
How correlated? I spent 2 minutes trying and failing to get chatGPT to generate code that downloads an image dataset and runs diehard on the LSBs. I'd expect the LSBs to pass the randomness test.
I think this topic is on a lot of peoples' minds, and it would be nice to get a discussion thread going about it with a quality article at the focal point instead of this completely uninformed one.
You can be thankful that your little bubble is still intact while wishing that there was a way to provide similar bubbles for the masses. I recently realized that the stability I have in my life, which I would've perceived as boring or mundane as a younger man, is more than I ever could have asked for compared to what most of the world gets, especially in times other than ours.
I select papers based on references from coworkers, Twitter posts by prominent ML researchers I follow, ML podcasts, and results.
The research becomes relevant immediately because my team is always looking to incorporate it into our production models right away. Of course it does take some planning (3-6 months) before it's fully rolled out in production.
