[FRIAM] temptation

[glen]

I'm tempted to actually give this a shot:

IsaAbduct: A Multi-Strategy Abduction Pipeline for Isabelle/HOL
https://hanielbarbosa.com/papers/2026fmcad-isaabduct.pdf

I've had a terrible time trying to use Lean. The SysAdmin is persnickety. But I naively believed Hansen in this comment

https://mathoverflow.net/a/513774

on Chow's post:
https://mathoverflow.net/questions/513742/are-we-stuck-with-lean

"the formal system of Isabelle/HOL itself suffers from things like a frankly confusing object theory/metatheory distinction that the user is supposed to be shielded from but is nevertheless exposed to often (at least in my experience)."

One of the things I really like about both OpenCode (depending on the model, of course) and Claude Code is their ability to exhibit what looks like abduction. Both tend to go down useless rabbit holes. But as long as I'm watching them and manually hand holding, their "maybe this is what's happening" or "we could try this approach" often works. But, again, I'm not doing math. I'm usually trying to plug tech together to achieve some previously conceptualized result. So I'm sure it's different.

-- 
8647 ⊥ ɐןןǝdoɹ ǝ uǝןƃ
ὅτε oi μὲν ἄλλοι κύνες τοὺς ἐχϑροὺς δάκνουσιν, ἐγὰ δὲ τοὺς φίλους, ἵνα σώσω.