661–670 of 681 posts
This is the second ChatGPT shared conversation I've seen today that is truly fascinating. The first one was someone proving another conjecture false by just repeatedly saying "keep going" to ChatGPT: https://x.com/DmitryRybin1/status/2079904005652893709 What a world we live in.
As promised elsewhere in the thread.
Earlier quoted context omitted.
It's a class with an array of integers in it with .length() == t - 1 and the same methods as Matrix. In lean4, even without mathlib4, TCP/IP is way more code than a Rees algebra. Math uses dense notation that is gigaoverloaded, and the disambiguating context was historically the leisure and proximity to have someone explain what the lexemes even mean. lean4 is proving to be very revealing as an uncorruptible referee…
That's false. Z[n] in rings does not mean "an array of integers of length n", it means the subring generated by Z union with {n}, where n is an element of some other set. For example: Z[ i ], the Gaussian integers, is the subring (of C) generated by Z union { i } where i is the imaginary unit in C, the complex numbers. The Gaussian integers correspond to the integer grid-points of the complex plane, if you want to vi…
Earlier quoted context omitted.
For mathematical research, you can just run until you have a computer checkable Lean proof.
Given that it was formalized correctly, which is far from trivial in many cases (Of course LLMs can help there, get it right etc, just a caveat that people have to keep in mind)
Earlier quoted context omitted.
The free market is mostly the glue that binds lots of tiny and not so tiny planned economies together. (I mean companies and even family budgets.)
As long as that N is high enough for each market, it’s good enough. When you are down to 3 producers, well there are reports of tigers there.
As a small wrinkle: the actual observed number of producers can be small, but the market still be competitive. See https://en.wikipedia.org/wiki/Contestable_market for one case: when potential suppliers are waiting on the sidelines.
Earlier quoted context omitted.
This is some work that I want to see in education. How do you validate if something is true or not. A lot of times that will take physical tests. Or in the case of math/logic, tests to validate each line or validated sources of previously proved theorems
You use the scientific method. Make a guess about how the system works, do experiments aimed to show that's not the case, adjust guess accordingly, and repeat
Earlier quoted context omitted.
It reinforces how to "learn AI" is to first master the problem domain. I can use AI for coding after decades of coding. I can't use it for theoretical physics because I can't evaluate the responses.
Correctamundo. That's EXACTLY what I just wrote about. And how we'll create the next generation of people who know how to evaluate responses when we're creating a generation of people who are increasingly reliant on LLMs to do the work makes for a strange paradox. https://larsfaye.com/articles/ai-coding-will-prevent-experti...
Industry reality is that for bespoke software solutions we have been running for decades on non-technical people straight out of a 5 day "boot camp" copy/pasting together "solutions" from SO, or "Sharepoint Configurators" cobbeling together a LoB process where is takes 3 minutes to get to the next screen with a 10% error rate etc.
Earlier quoted context omitted.
The most powerful way to use Fable in particular seems to be to pit it against Sol as a reviewer (or, I suppose, vice versa.) After going back and forth a half-dozen times, the result tends to be pretty much bulletproof. What's somewhat disturbing is just how much Fable's code really does benefit from the review. It tends to leave a lot of low-hanging fruit, and you can see it getting kind of impatient when repeatedl…
What are you using to put Fable and Sol on each other?
1) Fable generates updated .c sources and .md design documents in myproj_fab
2) A batch file in myproj_sol copies the updated files from myproj_fab to myproj_sol
3) I tell Codex to "Review updated files, write findings to review.md"
4) Sol rips Fable a new one, usually
5) Another batch file copies review.md back to myproj_fab, where I tell Claude Code "See review.md"
I don't want to automate it any more than that, because I'll get lazy, stop watching the tennis match, and miss something important. Which will probably happen anyway...
Earlier quoted context omitted.
Good writeup, and certainly food for thought. I wonder if this key point actually holds though: >The skills to do so, however, are a function of someone who has experienced the friction and challenges over time that culminate in "good taste". It's certainly sometimes true, but I don't think it's a general rule. Sometimes friction is just friction and sometimes you spend 1000 hours learning something that disappears a…
> Everything you know about 6800 assembly will not make your note-taking app any better. It could. It could make a simple note-taking app not take gigabytes of memory and take visible delay on each click. Most people don't bother of course because simple note-taking app is not worth the effort. It's possible to do better, it's just often not practical.
But the taste that tells you a note taking app should be fast doesn't come from your knowledge of assembly. It comes from using the app.
Being able to have an AI generate 8 variants of an UI and 5 variants of a storage mechanism is more helpful to reach the goal of a good note-taker. Trying out those prototypes and tweaking them to perfection is also friction, only it happens closer to your actual goal than doing quicksort in assembly.
There are of course examples where the friction does help, and where the "aid" of the tool deteriorates useful skills, but I think that will sort itself out over time. Useful skills will remain, useless ones will disappear, as they always have.
It’s endlessly fascinating to read the AI transcript of an expert who _really_ knows how to cut to the chase. It just shows how much you can potentially squeeze out of these models. I’m also surprised to see that even Terrence Tao seems to use it in a way that resembles, in progression, how I use llms in my area of expertise (emphasis on progression and usage patterns, not absolute skill, obv I don’t match that): sho…
It reinforces how to "learn AI" is to first master the problem domain. I can use AI for coding after decades of coding. I can't use it for theoretical physics because I can't evaluate the responses.