![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
dmmLean theorem prover seems to be the most convenient and practical (good enough for mathematicians to use it in real work, I am seeing plenty of such stories lately; there is a bit of controversy on whether to use Lean 3 or Lean 4).
The best quote according to "leanprover" twitter:
>Our favorite quote from the paper: "Monadic syntax is excellent for expressing stochastic algorithms, and working over finitely supported distributions avoids the need for integrability side conditions during proofs."
Links are in the comments.
The best quote according to "leanprover" twitter:
>Our favorite quote from the paper: "Monadic syntax is excellent for expressing stochastic algorithms, and working over finitely supported distributions avoids the need for integrability side conditions during proofs."
Links are in the comments.
no subject
Date: 2023-12-29 02:40 pm (UTC)https://arxiv.org/abs/2311.14125, "Scalable AI Safety via Doubly-Efficient Debate"
https://github.com/google-deepmind/debate
no subject
Date: 2023-12-29 04:11 pm (UTC)Ничего себе новости!
no subject
Date: 2023-12-29 04:44 pm (UTC)Теренсе Тао тоже всё время работает и с Lean, и с GPT-4, я читаю, время от времени, его https://mathstodon.xyz/@tao