seanhunter

I don't hate AI preprints, I hate slop grenades, which is what this is. Either you did that on purpose (which was what I thought looking at your website - that you created a honeypot to trap agents) or you don't realise that's what you're doing, in which case this makes me very sad.

I think (looking also at his website) that he is trying to make some sort of honeypot for agents. The lean code is completely nonsensical- tons of broken latex, dense references in the docstrings and the proofs are all very long names to obscure the fact that there’s nothing there. All they do is instantiate structures with lots of arguments and then assert one of the arguments.

Named after Kepler, who went from Tycho Brahe’s observational data to the laws of planetary motion (as mentioned in the article). But one really inspiring thing about Kepler is not mentioned there is that he started with a different theory and then changed his mind when the observational data showed he was wrong. We have the laws of planetary motion because of a feat of tremendous intellectual humility where a really smart person was prepared to admit that the theory they had invested a huge amount of time and effort into formulating didn’t match the observational data, _so they changed their mind_.

Kepler’s original theory was that the orbits in the solar system were defined by polygons and their inscribed/circumscribed spheres. This seemed very attractive because at that time they knew of 6 planetary bodies and this fitted in somehow (I don’t remember exactly) into this model with nested platonic solids and the spheres around them. Then Kepler realised that the predictions of this very elegant model were worse than the heliocentric model.

So when Brahe’s observations became available he basically threw all that out and started again, to develop his wonderfully elegant laws of planetary motion based around elliptical orbits which also have the significant benefits of predicting planetary motion beautifully and were later found to be entirely derivable from Newton’s laws of motion using calculus (there is a wonderful presentation of this derivation in Spivak for anyone who is interested).

For some reason I’m not allowed to respond to the child comment so I’m putting this here:

Perl 5 was released in 1994. Palo Alto Networks was founded in 2005, so Perl 5 was certainly available when they built their first products and would have been a superior choice to either PHP or Perl 4.

There are some (typically small) simplifications that computers are indeed good at. These could be thought of as analogous to compiler optimizations - they’ll see that your proof is basically composing several lemmas and that some of the work in the middle can be removed so it can just do that. In many cases with lean if you post a short to medium-length proof into an llm it can suggest these types of small improvements for you.

What they’re not that great at is the type of improvements that really make a big difference: big simplifications etc. This is not super suprising when you understand how this works.

Firstly proofs in lean (and I think many other assistants) are essentially functions which take hypotheses and instantiate a particular type. That type being equivalent (due to the Curry-Howard correspondence) to a proof of some proposition. The assistant uses dependent type theory to make sure all the types match up at each step, which is what makes it rigorous. So the task of simplifying a proof is basically finding a route through an infinite-dimensional space where you know your starting location and the desired end point, but at any step you can go in basically any direction you like so long as you can justify your step. You justify a step by either choosing from a (vast at this point) library of lemmas and theorems that are in your standard library, or by recursively building the proof/function you need to justify the step you want to take using this same process you’re trying to use for simplification. This is incredibly flexible, but means you’re actually spoiled for choice and planning is hard.

Secondly, in “pen and paper” proofs, LLMs don’t know the difference between steps which are important/easy/hard/intuitive/non-intuitive for human mathematicians, so lots of the proofs they produce are extremely clunky and pedantic in places and dwell for ages over details that are obvious and would usually be skipped over and then will move very fast through things that justify more attention. This unevenness is part of what makes their proofs hard for humans to work through, but also means they are generally poor judges of what would actually constitute a decent simplification.

Google wave was eventually released to the public but initially it required an invitation. So if you had a friend at google you could get in but if not you were out of luck. This killed early momentum and when they eventually opened up the product was dead on arrival.

Spending is supposed to be decided by congress not the executive branch so quite obviously yes.

It’s not an exciting advancement if it’s just the AI equivalent of google wave. It’s totally reasonable to be skeptical of marketing and want to try something for yourself.

I think there are a lot of practical applications where something that works few-shot and doesn't require training is quite appealing if the cost of inference is low. That's the sweet spot for Jev and similar models. If you have time and an eval set to train it, clearly a "real" special-purpose classifier should have much better performance (and for most applications cheaper cost/faster inference), but Jev and friends are way better than using a full-fat transformer LLM for a classification task.

As an example, I've been using winnow running locally as a decision model in openchamber to select between llms for doing various tasks. I don't have an eval set of different coding and other tasks that I could use to train a proper classifier. This I just download off huggingface and it works out of the box and has cut my token spend to a fraction of what it was. So it's good enough to be beneficial.

I have discoverd a truly marvelous RCE which this margin is too narrow to contain.