171–180 of 182 posts
Earlier quoted context omitted.
I recommend taking your own advice on that one, specifically the part about reframing efforts of strangers.
I take your views to be exactly as you state them.
Earlier quoted context omitted.
Not arithmetic or boolean algebra. What's your definition?
I'm not the one making obtuse claims and desperately trying to trigger reactions.
This is an interesting approach. My team has been prototyping something very similar with encoding business operations policies with LEAN. We have some internal knowledge bases (google docs / wiki pages) that we first convert to LEAN using LLMs. Then we run the solver to verify consistency. When a wiki page is changed, the process is run again and it's essentially a linter for process. Can't say it moved beyond the p…
For anyone curious about what LEAN is, like me, here’s the explanation: Lean Theorem Prover is a Microsoft project. You can find it here: https://www.microsoft.com/en-us/research/project/lean/
I had a surprising interaction with Gemini 2.5 Pro that this project reminds me of. I was asking the LLM for help using an online CAS system to solve a system of equations, and the CAS system wasn't working as I expected. After a couple back and forths with Gemini about the CAS system, Gemini just gave me the solution. I was surprised because it's the kind of thing I don't expect LLMs to be good at. It said it used P…
Probably the main deficiencies are confusion as the context grows (therefore confusion as task complexity grows).
"Alice has 60 brothers and she also has 212 sisters. How many sisters does Alice's brother have?"
But the generated program is not very useful:
{ "sorts": [], "functions": [], "constants": {}, "variables": [ {"name": "num_brothers_of_alice", "sort": "IntSort"}, {"name": "num_sisters_of_alice", "sort": "IntSort"}, {"name": "sisters_of_alice_brother", "sort": "IntSort"} ], "knowledge_base": [ "num_brothers_of_alice == 60", "num_sisters_of_alice == 212", "sisters_of_alice_brother == num_sisters_of_alice + 1" ], "rules": [], "verifications": [ { "name": "Alice\'s brother has 213 sisters", "constraint": "sisters_of_alice_brother == 213" } ], "actions": ["verify_conditions"] }
I had a surprising interaction with Gemini 2.5 Pro that this project reminds me of. I was asking the LLM for help using an online CAS system to solve a system of equations, and the CAS system wasn't working as I expected. After a couple back and forths with Gemini about the CAS system, Gemini just gave me the solution. I was surprised because it's the kind of thing I don't expect LLMs to be good at. It said it used P…
Earlier quoted context omitted.
Address the substance of my statements or save yourself the time & further keystrokes responding to my posts.
There is no substance to address lol.
Earlier quoted context omitted.
This is somewhat unusual: 28% on the Tomatometer, but 7 out of 10 on IMDb. Beyond its relevancy to the parent comment, would you consider it a good movie yourself? (for a random/average HN commenter to watch)
It didn't do well critically, but audience scores on many platforms are 60-70%. It came hot on the heels of The Matrix, has similar themes, but nowhere near as ... everything compared to Matrix. I'd bet the only reason it did so poorly critically is due to the timing of the release. It's a fine movie though.