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 μὲν ἄλλοι κύνες τοὺς ἐχϑροὺς δάκνουσιν, ἐγὰ δὲ τοὺς φίλους, ἵνα σώσω. .- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. FRIAM Applied Complexity Group listserv Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom https://bit.ly/virtualfriam to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: 5/2017 thru present https://redfish.com/pipermail/friam_redfish.com/ 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/
