Post #2522095
2026-05-10 09:10 UTC
That was a fine show, thank you all.
A side question, since this matter came up as a side note:
If LLMs make lots of proposals of mathematical proofs,
how feasible might it be to get them to submit those proposals
in a formal language, so they can be fed directly
into a proof assistant or a proof checker or something like that?
I can imagine several reasons why it wouldn't be feasible,
but I don't know enough about these matters
in order to offer useful thoughts.
And I quite understand that I should probably ask this elsewhere,
at the appropriate junction etc.
@screwlisp@gamerplus.org @bagder@mastodon.social @albinowax@infosec.exchange
Replies (2)
-
@screwlisp@gamerplus.org 2026-05-10 09:18
@vnikolov@ieji.de @bagder@mastodon.social @kentpitman@climatejustice.social Sorry I didn't catch your toot live, hopefully people can kinda pick up here. Actually, we had a quick conversation to the effect of what you just said right afterwards (or something like that). #archive https://toobnix.org/w/rPKt4GRBwLeWzF3VcMFWNo
-
@kentpitman@climatejustice.social 2026-05-10 09:21
@vnikolov@ieji.de @screwlisp@gamerplus.org @bagder@mastodon.social @albinowax@infosec.exchange It seems not an individual program question but almost a question about the entire structure of the applied math field, like asking accountants their posture on spreadsheets and their use in forecasting back when they were a new tech.