[astrange]

Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.

[YeGoblynQueenne]

What are the search algorithms then? DFS, BFS, A*, etc, can you name them?

[tptacek]

Why are you asking them which basic computer science graph traversal algorithms a frontier model used?

[YeGoblynQueenne]

OP:

>> using human-like(?) reasoning means cutting down the search space by having some sort of insight or intuition which allows you to prune branches from the entire tree

So according to the OP there's a search of a tree and it also uses pruning btw, so I want to know what search they mean. Why are you asking?

[tptacek]

Because your question doesn't make sense; this isn't how implicit search works.

[YeGoblynQueenne]

"Implicit search" with pruning?

[wmorgan]

Why not? Lasker said, “when you see a good move, look for a better one.” That was tree pruning advice for an implicit search.

[tptacek]

I don't understand why you're scare quoting "implicit search".