Claude, GPT, and some open models are fluent in the iterative use of Lean 4. In a derivation, they can offer commentary on the motivation for each step inline – they write comments -- and then use Lean to check/elaborate. Or they can explain after the fact the trajectory of a derivation. So, I find it strange and more than a little suspicious, the criticism that the AI companies aren’t aligned with the mathematics community. If anything, loosely directed use of frontier LLMs leads to hundreds or thousands of pages of rigorous corollaries that go in all directions. Paraphrasing a concern of the community, the wander-around-and-discover-stuff activity they’d prefer to do (professionally) and not merely absorb the utilitarian outputs of a model directed toward a single goal. What they are conveniently not mentioning is that the wander-around-and-discover-stuff activity is accumulating at superhuman speed in AI notebooks on behalf of goal directed behavior. It sure seems like it was ok when the party was only over for the coders, but then the sand shifted on the math guys too and then it was all a great outrage.
From: Friam <[email protected]> On Behalf Of Jon Zingale Sent: Monday, September 28, 2026 8:36 PM To: The Friday Morning Applied Complexity Coffee Group <[email protected]> Subject: Re: [FRIAM] Circuit bending I certainly don’t mean to imply that I work this way because it’s demonstrably better. It’s a habit, and a way of working with LLMs that I can get my head around. Many of my friends are going the harness route, generally with mixed results. To some extent, I think my habit is related to how I like to work with my own mind. I’m not sure I can elaborate meaningfully on that right now, so I’ll leave it there. What I can offer for debate is that I think the harness direction of development would benefit from more thoughtful type-theoretic foundations. I don’t mean the trashy, just-trying-to-get-funded version that Jev is hand-waving at. I mean properly good type theory of the kind I know you know.
smime.p7s
Description: S/MIME cryptographic signature
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. 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/
