Cautionary note (and a serious one, not to be snarky): Being well off financially is not a protection against gambling addiction (which can also take the form of day trading, for example); which is a pretty efficient way to ruin ones financial wealth, amongst other things.
As with many other psychological phenomenona, finances and education only protect to a certain degree or not at all, depending on what one is talking about in detail.
This is not a comment about correlation or causation of wealth with mental health, but rather a warning to keep in the back of ones head; success and a sharp mind don't make one immune against mental health issues in general and gambling addiction in particular.
To me, the difference is a form of classism. Addiction to drugs is for the lower class. Addiction to gambling from making money from investing is something only upper class people can have.
I feel like this is just straight from the Kalshi marketing department. The wealthy make money from speculation by taking calculated risks and offsetting those risks with other investments. They're not betting everything on black at the roulette table or bettin on the outcome of football games.
Always nice seeing others arriving at similar conclusions! Those two jump out to me:
- "Most compilers hard-code a cost model. Vx reads one. A machine file describes the memory hierarchy and interconnect of a real part, and the compiler admits or rejects placements against it." I also designed it so that the target system is described by a single file that is picked up by the static analysis - cool!
- "Where data lives is part of its type" also doing that - when I got my project to an mvp state; I need to check out how vxlang does what it does: do they use a literal typesystem, or also compile checks outside of that? If its a type system, is it a dependent type system, or another flavor?
Yet another motivation to finally get my side project starting (forth-adjacent, many similar claims with regards to compile-time checks as vxlang; however, I still have to achieve that, while they already seem to have at least those and more in place; kudos to the vxlang team!)
The main problem I see with RC which has prevented me from applying is there’s no stipend or housing. Most people can’t afford a summer in NYC without pay. So I’m not sure who the target audience really is, I guess wealthy SV engineers.
Not really something you can control, but RC always feels "unauthentic" whenever people write about it.
It is often portrayed like an old-school hackerspace or makerspace but it's definitely not. It has an explicit corporate background, and it always feels like that is somehow hidden.
In these comments there is a comment that claims that RC is not for business builders and networking, then immediately gets disproven by a quote from its very website. This shows that you have an actual image/brand problem.
It is similar to how the term "hackathon" evolved. In the old times it was people coming together who worked on shared goals (like a FLOSS project) but only communicated via mailing lists and probably would never met in person otherwise. A hackathon was often an emotional thing, involving poor people travelling to the other side of the planet to meet their online friends to drink beer and finally have a whiteboard to communicate some complex ideas. Then corporations came and organized soulless "hackathons" and turned it into an idea farm and talent recruitment. The term "hackathon" is pretty much burnt completely nowadays.
So anything that feels like it gets subtly used by corporatism just naturally gives techies the ick. It is not the first time this bait-and-switch happens, so people are fair to assume intent.
I say you cannot control it, as obviously the public image comes from those blog posts of RC "Alumni" (Another great example: that term alone gives me the creeps). And those people have the right to feel excited about a nice experience that it probably was for them.
But Recurse Center should probably be proud of the corporate background and actively counteract the impression of being a hobbyist makerspace that just has better inventory and manpower.
> Please do not ask the LLM to break the universe :)
Eh, every school db should be able to service a student called "Robert'); DROP TABLE Students;--", and every public facing LLM should still work even if asked to calculate the last digit of pi - that fulfills two noble purposes: 1) is fun and teaches whoever is responsible for the service some valuable lessons in craftsmanship or 2) if the service is built robustly (i.e. simple token limit and time limit per user), that's an easy way to gain street cred
It should obviously not come as a surprise that having areas of the brains working differently can explain an awfull lot of things... but to answer your question directly, yes of course of course there are!
Simply look up all the many, well
-supported and -researched known correlations with ADHD first. In the second step, you can construct the set of all possible correlations, and subtract the well-researched ones if it. What is left is the set of correlations that are either not explained by ADHD (the big majority I would assume) or explained by ADHD, but as-of-yet unknowingly so.
This might be a bit anticlimatic, but clinical psychology is pretty straightforward study design and statistics, and set theory is not that new either, so... no big surprises I am afraid.
100% agree on the ad angle. Ads normalised using digital products/services by paying with data and attention.
That is one of the reasons why I would love to see - reasonably priced - paid services, or even have governments offer them (as in: Source is open, hosting is being paid by the government). Given the role social media, the internet and so on plays today, it might make sense to treat this as a common good.
But that side track aside; I think that privacy respecting, ad free products can be offered for cheap, if their goal is only to finance themselves, development and gain a small margin. And true, network effects / buyin is real, but I also think that the market for ad-free digital spaces/services will continue to grow, as hopefully people become more and more aware of how precious and limited their attention really is.
> I suspect that the next big AI breakthrough will result at least in part from constraining LLM decisions with old AI approaches. Frank Coyle presented the idea of ontologies constraining LLM output about a month ago: https://www.youtube.com/watch?v=Sir59K8ZDPU
Interesting, thanks for sharing!
I plan to give it my own shot with vibing my own harness; I plan to use https://glean.software/ as the central database for everything code, then for documentation. After that, it could be used for bookkeeping for reasoning in a style similar to what you describe; after all, Angle, the query language of Glean, is a https://en.wikipedia.org/wiki/Datalog with some extras (I don't know which yet), so stuff like onthologies could be queried quite well, I would guess.
If you mean letting an LLM generate code for a Prolog planner from an English problem description, that has been done successfully already with last year's models eg [1].
Appreciate the link! That is not what I had in mind though; for them, the Prolog Code is the goal, for me, Prolog is an interface language within a system I build. That code could be generated on the fly, but I lean more towards fixed templates that can be instantiated by input some variables by the LLM that is doing agentic code, rather than having that LLM reproducing that query code completely on the flow.
The reasoning behind it is that I want to put as much logic as possible into the harness where it is deterministic, controled and fast - My goal is to make agentic coding usable for my purposes even with small local LLM models. Those might botcher generating Prolog queries sometimes, but they might might be able to used my API/interface/whatever reliably (and then the harness does everything else under the hood, including instantiating the Prolog templates and running the queries)
Hmm, I would say even older than that (which, of course, is in no way intended to be a value statement of any kind, I like the website and the project, cool idea! :D).
If you squint a little, the linked project is basically a https://en.wikipedia.org/wiki/A*_search_algorithm with optimized implementation, heuristics and so on. I also think that A* was associated with AI due to its use in path finding in early robotics - But I am not sure!
> This is extremely unconvincing. Manual review of 10,000 lines of AI generated code is a terrifying prospect.
With https://en.wikipedia.org/wiki/Lean_(proof_assistant) (and other proof assistants), you need to review only the lines that correspond to the theorem that you want to prove and their types (I am not very experienced when it comes to lean, but I would assume that comes down to a few hundred lines of code, at most). The rest is left to typechecking (which, I would expect many in the field to agree, is at as reliable than your average peer review process in professional mathematics, and likely much more). That's the reason why Lean4 is making such a fuzz now.
That itself is not trivial too, but way easier than reviewing every function and definition used to prove that the theorems have indeed the types they claim.
If one accepts the proof of the https://en.wikipedia.org/wiki/Four_color_theorem, then there should not be new reservations these proofs; except from the maybe new additional failure scenario that the authors (still correctly!) proved theorems that don't state what they think they stated.
To sum it up: There is IMO no domain more suited for using LLMs than mathematical proofs that can be formalized using Lean4. The fact the hype-circle started earlier in software than in maths is due to the difference in monetary incentives I would assume. (Or another, rather radical and not really serious phrasing: "When it comes to Lean4 proofs that typechecks, there is no AI slop" - the theorem being proven might be uninteresting, but the proof itself is very very very very likely to be correct)
> “byte-for-byte equal”
The term itself or its association with LLMs? I would get the latter, if its the former: It's an desirable property to have, I always like seeing people going that far (assuming obviously that they indeed did so, and in the places where it matters!)
> you need to review only the lines that correspond to the theorem that you want to prove and their types
This is (unfortunately) not actually the case—just a few weeks ago, someone "proved" the Collatz conjecture via a Lean proof 1) whose theorem statement was correct, 2) typechecked, and 3) was even verified by external tools with their own implementations of the kernel.[0]
The problem was (AFAIK) that the Lean kernel has a lot of fancy features that aren't yet perfectly understood from a type-theoretic perspective (I don't think Lean is unique in this regard; pretty sure Rocq and Agda are in a similar situation). And so when the kernel implements some feature whose soundness isn't guaranteed, the independent verification tools (or at least some of them) follow suit, and now any issues in the former affect the latter as well.
Huh. Thanks for bringing that into my attention, and the link!
Yes, in hindsight it makes sense that a eager LLM would exploit bugs in the kernel itself. I have not read the details yet (but want to!) and assume that it is rather related to the layers directly before or after the type-theory core; i.e. that the AI managed to get a correct typecheck by sidestepping a check during in one of the translation steps somehow, by manipulating the kernels result or by going totally hacker mode and swap implementation/overwrite memory; that is just speculation on my part though, I mainly base if on what I know about Haskell and the https://en.wikipedia.org/wiki/Calculus_of_constructions in general that have not that many constructs, and I would assume the variants used in Rocq and Lean are proven sound.
For experimental features where soundness is not proven, all bets are off IMO, but of course, that does not stop bad actors from engagement knowlingly abusing unsoundness for their own gain. Fortunately, that kind of manipulation is easy to verify when one has access to the codebase; I am would assume that something like lints for experimental features exist, or better even, something like a "sound mode". That does not help against hacking the kernel machinery though.
Concluding notes:
- In this particular instance, the Collatz conjecture was appearently chosen on purpose to demonstrate the Kernel bug, from the same thread: "Not that this changes any of the above, but I am informed that the person posting the proof was actually aware that this was a Lean kernel soundness bug, and it was not intended to be taken seriously as a solution to Collatz's problem."
- IF the code is made public (and it would be highly suspicious if parts of a proof where hidden), then I would assume this kind of hack is 1) easier to spot that other kinds of hack, since the asset-under-attack is really small and 2) there is not so much incentive to use much time/ingenuity/tokens on finding those hacks (the more are found and fixed, the better of course) 3) and they should be easy to defend against, I would assume; my first thought would be the flag I mentioned above that simply forbids all non-sound features, at the cost of limiting expressive power.
----
Edit: I checked, and I think it alleviates my worries in the sense that the bug(s) where not in the type theory or its implementation, but rather the machinery around it. Further context below:
The following is from that thread or links from it:
- "Fixes two things: (1) more strict/nuanced handling for structure/proj interactions, and (2) adds methods for enforcing that generated auxiliary data for inductives, constructors, and recursors are more strictly checked against the assertions in the export file." | That is the fix to the non-Lean-kernel that was mentioned. To me, (2) looks firmly like what I meant with "supporting machinery", regarding (1), I do not know enough to have an opinion about it (i.e. how on what layer those interactions happen(ed)) | https://github.com/ammkrn/nanoda_lib/pull/22
- "For example, pipeline wedges (execute this instruction and the core freezes and never executes another instruction) would not be found by these techniques..." | Power and limits of Lean | https://infosec.exchange/@david_chisnall/117003914014196496
- "@mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it. There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer." | Computer-checked proofs run on computers, which brings its own attack vectors, independent of how well the kernel is written | https://infosec.exchange/@0xabad1dea/117002712346315184
personal, cautios takeaway after reading the details: If you use Lean4 to write proofs, or read that a reputable group of mathematicians publizised a Lean4 proof, you are still highly unlikely to be fooled by a bug, and if Fable 5 decides to exploit a 0day in the core Lean4 machinery, that should still be able to be caught quickly.
As with many other psychological phenomenona, finances and education only protect to a certain degree or not at all, depending on what one is talking about in detail.
This is not a comment about correlation or causation of wealth with mental health, but rather a warning to keep in the back of ones head; success and a sharp mind don't make one immune against mental health issues in general and gambling addiction in particular.