Item — HN Reader

>>A good sign that LLMs have reached human level for a much wider class >> of problems will be if they start proving theorems using methods that, like much of the very best human mathematics, are new and surprising but that with hindsight come to seem beautiful and natural.

I must be taking crazy pills and the AGI surely will pass me by... But TODAY, middle August 2026...And in the context of testing and evaluating the capabilities of current SOTA models to implement an Agentic application for job search, here is some simple inhouse built evals I run today, since I don´t trust LLM vendors published benchmarks...

Models tested: GPT-5.6 Sol in Extra High mode and Opus 4.8 Max.

TASK REQUEST: Clear, not too long not too short prompt, for LLMs to go out and research freelance consulting gigs for one specific IT domain, and in one specific country in Europe, including maybe opportunities driven from temp agencies based in geographically close countries.

RESULT: Models go out, fetch the data, and completely misunderstand the task...offering on first results, permanent roles instead of freelance, and based on the country where the agencies are, not in the one it was request for. Think for example IT jobs in Ireland, while freelance agency in London.

ANALYSIS: No intelligence I can call it shown by models, adding cognitive effort for human in the loop to detect subtle factors, and therefore totally useless for agentic app...Best practices would be I guess to add agents on top of agents but although in the p95 of cases that will reduce the errors...for the remaining 5% that could have hallucinations or logic hallucinations like these ones, compounding on top of other logic hallucinations.

I dont care about the theorems being proven. At the end we will found out what most mathematicians were doing, was just exploring the same combinatorial and abstraction patterns. And because of that I am sure LLMs will make mince meat of a lot of mathematical domains.

But right now, what we call intelligence is not existing where it matters, and Ed Zitron is right its a parlour trick.

8 comments

Stop wasting your time and use actual code for most of what you give an LLM to do. Make them write the code even.

Anything that can be verified mechanically should be code. Only use LLMs to fill in the gaps where things are fuzzy. Don't fall for the idea that those harnesses are general purpose, make your own fit to your task with the guards and verification steps you need. Make the LLM create the harness even.

There is no amount of markdown that can make a machine generating plausible text generate truthful text, it just happens to be truthful because of what it was trained on. Nothing coming out of an LLM should be taken at face value.

The propaganda about LLMs being intelligent and able to "reason" is only serving the companies selling you tokens to waste on "prompt engineering".

The irony about your comment is that, this is probably the most likely opinion and most consensual around many technological practitioners.

But the mathematicians here in this thread, are having a hard time with these clearly dumb models, doing so well in proving theorems in their domains :-)

Writing code and proving theories are flip sides of the same coin. See e.g. Phil Wadler’s “Proofs are Programs”: https://philarchive.org/rec/WADPAP

The statement should probably really be “programs are proofs” since it’s difficult to make it a true bidirectional isomorphism, which is why the underlying principle is properly called the Curry-Howard(-Lambek) correspondence: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

The point is that the fact that LLMs are good at writing code directly implies that they should also be good at certain classes of mathematical proof.

Not in any useful way, though. In the Curry-Howard correspondence, being able to write a function of type "int -> string" proves that there is at least one valid string or there are no valid ints. The code of the function is a proof of this statement. For example you might prove directly that there is a string, by writing return "hello"; or you might write return bool2string(int2bool(myInt)); thus chaining two implications to arrive at a shortcut implication.

> Not in any useful way, though.

Theorem provers and proof assistants like Lean, Coq/Rocq, Agda, Idris, NuPRL and Epigram all fundamentally depend on Curry-Howard.

And again, the point is not that there’s some magical isomorphism, but that if LLMs are good at coding, they’re also likely to be good at certain classes of proof.

No they don't. They act on proofs, not on stupid conversions of proofs into useless programs.

You should take a look at "The Calculus of Constructions" (1988), which is one of the seminal papers that describes the basis for the Coq (now Rocq) theorem prover: https://www.academia.edu/47789825/The_calculus_of_constructi...

Here's a very relevant quote from the introduction:

> "The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a lambda-expression, typed with propositions of the underlying logic. By removing types we get a pure lambda-expression, expressing its associated algorithm. Computing this lambda-expression corresponds roughly to cut-elimination. It is our thesis that (as already advocated by Martin-L6f [36]) the Curry-Howard correspondence between propositions and types is a powerful paradigm for computer science. In the case of constructions, we obtain the notion of a very high-level functional programming language, with complex polymorphism well-suited for module specification [8]. The notion of type encompasses the usual notion of data type, but allows as well arbitrarily complex algorithmic specifications. We develop the basic theory of a calculus of constructions, and prove a strong normalization theorem showing that all computations terminate."

In other words, proofs are expressed as typed lambda terms, i.e. "proofs are programs". This is literally what such theorem provers are: examples of the Curry-Howard correspondence in action. If the correspondence didn't exist, none of these tools would exist.

Here are a couple of quotes from one of the Lean papers, "Theorem Proving in Lean", https://leanprover.github.io/theorem_proving_in_lean/theorem... :

> "This is the approach followed in the Calculus of Constructions, and hence in Lean as well. The fact that the rules for implication in a proof system for natural deduction correspond exactly to the rules governing abstraction and application for functions is an instance of the Curry-Howard isomorphism, sometimes known as the propositions-as-types paradigm."

> "The match statement is part of Lean’s function definition system, which provides convenient and expressive ways of defining complex functions. Once again, it is the Curry-Howard isomorphism that allows us to co-opt this mechanism for writing proofs as well."

All of the other theorem provers and proof assistants I mentioned rely on a similar approach.

https://claude.ai/share/f0c5c3c9-1882-44b1-b30e-fb427a0df472

I don't know your prompt and setup, but my claude had no problems doing that task. The search index isn't live, so it can't find current gigs, but that is a tooling problem.

I'm not sure why exactly, but I've heard the same from every single person using LLMs for anything related to jobs. The posting says it needs at least a B.S., and the LLM denies an applicant because they have an M.S. The posting thinks it needs 3yrs of work experience in XYZ technology, and it won't add it to the candidate's list because it doesn't have the context that the HR/LLM filter on the posting adds a bunch of nonsensical requests or that some other combination of skills makes the candidate stand out above and beyond that missing "requirement." And so on. The quality is quite poor.

On the other end of it, something like 80% of resumes I receive right now are clearly hallucinated -- referencing accomplishments that are copy-pasted from the novel-to-our-company thing in the job description a candidate will be working on, usually claiming they did XYZ at big tech a decade before the thing existed, or similarly with languages and skills. The resume "tailoring" process just manufactures lies rather than tailoring actual experience to the actual job.

Reading the responses to your comment the discussion would be a lot more productive if you shared your logs (preferably several of different top models since that's what you're claiming) where LLMs fail at this. Not very useful for people to go back and forth speculating on what you could have asked and with what formulation. As it stands for me simdezimon's logs are pretty definitive that there shouldn't be any problem for current capabilities agents to solve the task.

LLMs have no sense of geography. They measure distances between parts of words, not distances between parts of world.

“Canada is north of the United States” has a higher probability of correctness than “Canada is east of Greenland.”

This is an off topic rant unrelated to mathematical ability which is a closed problem often with complete logical information.

> TASK REQUEST: Clear, not too long not too short prompt

Why do you think there's such a thing as too long for an LLM prompt? You'll run into context window limits at some point, but the more verbose you are with what you ask of it, the better the results will be.

>> t the more verbose you are with what you ask of it, the better the results will be.

Trivially falsifiable:

"Context Length Alone Hurts LLM Performance Despite Perfect Retrieval"

https://aclanthology.org/2025.findings-emnlp.1264/

"Large Language Models Can Be Easily Distracted by Irrelevant Context"

https://arxiv.org/abs/2302.00093

>TASK REQUEST: Clear, not too long not too short prompt, for LLMs to go out and research freelance consulting gigs for one specific IT domain, and in one specific country in Europe, including maybe opportunities driven from temp agencies based in geographically close countries.

As a human, not an LLM, I could interpret "including maybe opportunities driven from temp agencies based in geographically close countries" as meaning "including opportunities in nearby countries outside of Ireland" (that happen to be driven by temp agencies).

Before writing off LLM as simply a "stochastic parrot" or a "parlour trick" remember it can't read your mind, not yet anyway.

I am describing the contents of the prompt that was not the prompt. The prompt was very clear to the model that some freelance opportunities in country A, the only one in consideration could be available via agencies in country B and C. And it was a clear prompt.

So what happen is a prompt said for example, find freelance opportunities in Ireland but keep in mind some of these might be available via temp agencies in London.

If you offer me not freelance but permanent roles, and not in Ireland in London...that is a logic failure.

Its this type of complexity with the normal world, that these SOTA constructions so badly fail at, and so spectacularly fail at the margins... despite maxing all benchmarks...Parlour trick.

Based on the rest of your writing I’m going to assume that the prompt was the problem.

He was perfectly clear in both cases.

If a human misunderstood this, they'd be a dumb human.

For perspective, I agree with the GP. The writing is not perfectly clear. We don’t have enough evidence to know if that was part of the problem.

Keep deluding yourself, unless you work for an LLM provider...

"Frontier LLMs Still Struggle with Simple Reasoning Tasks" https://arxiv.org/abs/2507.07313

"General365: Benchmarking General Reasoning in Large Language Models Across Diverse and Challenging Tasks" https://arxiv.org/abs/2604.11778

"...General365, a benchmark specifically designed to assess general reasoning in LLMs. By restricting background knowledge to a K-12 level, General365 explicitly decouples reasoning from specialized expertise. The benchmark comprises 365 seed problems and 1,095 variant problems across eight categories, ensuring both high difficulty and diversity. Evaluations across 26 leading LLMs reveal that even the top-performing model achieves only 62.8% accuracy, in stark contrast to the near-perfect performances of LLMs in math and physics benchmarks..."

Keep deluding yourself, unless you work for an LLM provider

You're clearly operating in bad faith, but just for the record: the General365 problems are very difficult as you can see from the examples at https://arxiv.org/html/2604.11778v1#A1. It's actually impressive that Gemini 3 Pro got 62%, and the strongest OpenAI and Anthropic models they tried were GPT-5.1 and Sonnet 4.5.

I found it very difficult to parse your description, "Clear, not too long not too short prompt, for LLMs to go out and research freelance consulting gigs for one specific IT domain, and in one specific country in Europe, including maybe opportunities driven from temp agencies based in geographically close countries."

( I was trying to quote a single sentence and then realised it ran on for the whole paragraph. )

Given how difficult I found that to follow, are you sure your prompt is actually "Clear, not too long not too short"? We now only have your word for it. I too had assumed that was a prompt given to an LLM to further prompt agents.

You can easily test this yourself with the SOTA models....or read the corroborating literature...

"General365: Benchmarking General Reasoning in Large Language Models Across Diverse and Challenging Tasks" https://arxiv.org/abs/2604.11778

What proportion of the human population could answer the example from that paper?

    Question: Strangers A, B, C, D, and E line up from youngest on the left to oldest on the right. Their clothing
    colors and shoe colors all differ, and they come from five different regions.
    Known facts:
    1. A is from Morocco.
    2. D is five years older than B.
    3. E is older than A.
    4. C stands next to D.
    5. A stands next to B.
    6. The person in teal shoes is not adjacent to the person from Vanuatu.
    7. One twelve-year-old wears yellow shoes.
    8. The person in orange shoes wears white clothing.
    9. The person in blue clothing is from Chile.
    10. The youngest person wears red shoes.
    11. Counting from the right, the fourth person comes from South Africa.
    12. E wears yellow clothing.
    13. The person in green shoes does not wear multicolored clothing.
    14. Two people are twelve years old, ordered by birth month.
    15. One adult is thirty-five years old, and that age is sixteen less than the combined ages of the other four.
    If you multiply every possible age C might have, what number do you obtain?

What does "The person in green shoes does not wear multicolored clothing" even mean?

Nowhere is "multicoloured" defined, are we to assume it should be treated as a colour and implied that someone else must be wearing "multicoloured clothing"? Because strictly that doesn't logically follow, and it ought to be phrased as "The person in green shoes is not the person wearing multicoloured clothing" if that is the case.

This is an extremely hard logic puzzle, especially since it's revealed at the end that there are multiple solutions.

I'd expect anyone to struggle unless armed with prolog.

> What does [ 13 ] even mean?

It means that it is possible for someone to be wearing a white shirt and yellow pants (say), but the person in green shoes came from the set of a Wes Anderson film.

That's cute, but it's driving me crazy, I guess I'll have to sit down and solve it to figure out how it's meant to be clued, assuming it's not just a red-herring entirely.

No offense to you, but we had to do these kind of exercises in grade school on days when a sub was in. You'd get together in a group and work through the logic puzzle on a structured form (i.e., it let you represent what you know about the person wearing green shoes, or the person from Morocco, etc.)

I'm familiar with the format, I grew up doing these, published monthly under the name "Logic Problems" in the UK.

My issue with this particular puzzle was the ambiguity of that particular clue, it's as if it got re-written or badly translated, because clue 13 as written carries no information.

This is a neat puzzle but you really don't need prolog. Spend a couple minutes thinking about it and you can solve this just fine.

Your question: It just means they have both green shoes and clothes, probably.

It's aimed to confuse a model with a bunch of information you-just-don't-really-need. The trick is to fish out which hints are more important than others. The order in which you apply them matters to make the puzzle easy vs. very hard. Which things give you the most amount of 'useful' information?

Call the people p1 to p5 (p5 oldest, p1 youngest).

Start with (15). This identifies the total age as 35+51. Now combine in (14), and you have 51 - 24 = 27 remaining years. This means the 35-yo is the oldest person, p5 = 35. Now add in the interesting thing that D = B+5. If you know that there is 27 years left to give to the two unknowns, B can't be 30 (or, D can't be p5). That means that D is 17 and B is 12 or D is 12 and B is 7.

This leaves three possible answers for the list of ages. Two of these are 7, 12, 12, 20, 35, or 10,12,12,17,35. The third one involves the case where the people other than the 12-year-olds and the 35-year-old are 5 years apart, in which case they can only be 11 and 16.

Combining all the 'stands-next-to' information (including point 2 which means D is to the right of B), we have eight possible orders: (AB)E(CD) or (AB)(CD)E. The last set of four is the only valid possible one as we know that D is not the eldest, which means E is 35. If the order is BADCE then B=7, A&D are 12, C=20, E=35. If the order is ABCDE then A=10,B=12,C=12,D=17,E=35 There's also the possibility that the 27 is made up of B and A (BACDE) are 11 and 16, and you are left with B=11,A=12,C=12,D=16,E=35. There is the possibility of the order being ABEDC. However, this carries no real consequences other than the clothing and shoes needing to be shuffled later. There's still only one possible value for the age of D. I'll leave the explanation for that variant out of the rest of the solution, the logic is roughly the same just with the clothes and country all juggled up.

Now one thing that's kind of unclear though is point (15). "One Adult". You'd need the definition of 'adult' to be a bit more precise (varies by country!), and also what kind of English is used to know if this implies there are at least 2 adults. If it does, then there is only one answer: D is always 12, since you need the 20-year-old to exist to have more than one adult.

If not, then D could be either 12 or 16 or 17, so the answer (so far) is 12x16x17 = 204x16=1224.

Now let's deal with the clothing, country, and shoes. All we need is that A is from Morocco, and that the second person is from South Africa. You can't simultaneously be from both places, which means A can't be in the second position.

That also clears up the ambiguity whether the 17 year old is an adult here (apparently they are), so that leaves only one possible combination: A,B,C,D,E, being 10,12,12,17,35. The answer to the question is 17.

Bonus: There's some extra stuff about countries and clothes: we have to check if there exist a valid solution that will fit with our one test. You could assume that the puzzle has an answer, but sneakily: that answer could be zero. If there are no solutions, there are no possible ages C could have, and so the answer is zero (or 1,depending on how you interpret the math of multiplying the empty set) . Here's one order that's possible (there's more, I'll leave it as an exercise to find the others):

Person: Country, Clothes, Shoes A(10): Morocco, Unknown, Red, B(12): South Africa, White, Orange C(12): Chile, Blue, Yellow D(17): Unknown, Green, Green E(35): Vanuatu, Yellow, Teal

(6) is the only point that's maybe a bit debatable? It's not true since the person wearing the teal shoes IS from vanuatu.

If this isn't valid solution for (6)... then there are no solutions, and the answer is actually 0. I'd go with 17 though, it seems fine.

> The answer to the question is 17

Except, according to the linked paper, the answer to the question is 420.

I got to 420 too, but only by ignoring almost all clues: https://news.ycombinator.com/item?id=49271594

A puzzle where nearly all clues are badly defined or irrelevant is not really a puzzle.

Super interesting, thanks for the reference.

I particularly found the note about “local collapse” helpful (near the end of section 3). The idea is that even though benchmarks contain a wide variety of different reasoning tasks, each individual problem requires only a few skills - unlike this benchmark where they deliberately construct tasks that span many categories.

That was not the prompt.

I know that. We don't know what the prompt was. We only have a self-assessment of the quality of the prompt from the person who wrote it.

It sounds like they're hitting a data source quality issue, which is hardly uncommon in scraping.

It's common for job boards to obscure who the real clients are, and if the scraping engine is LLM powered ( rather than LLM written ), then I would expect it to accidentally present agencies as the contracting organisation sometimes.

Breaking down the process so you can inspect the messy middle of a data pipeline is an important part of software engineering, but it sounds like they've tossed a messy task at an LLM and expected it to be proficient end-to-end.

Would the llm work better if it was given the job ad and asked where the job was located?

It seems to me that such simplified tasks tend work better. The rest of the loop is just scraping websites, which doesn’t really have a reason to rely on ai agents.