Mastouille

0 message0 participant0 message aujourd’hui

Jesper Agdakx 🔸Oh hey, Asterisk has an article on theorem provers, LLMs, and autoformalization (i.e. automatically turning math papers into formalized proofs). I still think this task is significantly more difficult than what some people seem to think, but who can really tell anymore at this point. <a href="https://asteriskmag.com/issues/09/automating-math" rel="nofollow noopener noreferrer" target="_blank">asteriskmag.com/issues/09/automating-math</a> <a class="hashtag" href="https://agda.club/tag/theoremprovers" rel="nofollow noopener noreferrer" target="_blank">#TheoremProvers</a> <a class="hashtag" href="https://agda.club/tag/coq" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a class="hashtag" href="https://agda.club/tag/lean" rel="nofollow noopener noreferrer" target="_blank">#Lean</a> <a class="hashtag" href="https://agda.club/tag/isabelle" rel="nofollow noopener noreferrer" target="_blank">#Isabelle</a>

Jesper Agdakx 🔸My PhD student Sára and I are looking for people to participate in a study on usability aspects of interactive theorem provers. Please consider signing up!Who? anyone who uses or has used an interactive theorem prover for whatever purposeWhat? 90 - 120 minute interviews (possibly including a small think-aloud programming session)When? interviews will be scheduled starting September 2024Where? online (participants from anywhere are welcome)We are hoping these interviews will help us determine how you interact with your theorem provers and to gain insights on how we can improve the user experience. We are interested in all aspects of interactive theorem provers, including but not limited to their design, their tooling, their libraries, and their documentation.Sign up here: <a href="https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy" rel="nofollow noopener noreferrer" target="_blank">https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy</a><a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a class="hashtag" href="https://agda.club/tag/coq" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a class="hashtag" href="https://agda.club/tag/lean" rel="nofollow noopener noreferrer" target="_blank">#Lean</a> <a class="hashtag" href="https://agda.club/tag/isabelle" rel="nofollow noopener noreferrer" target="_blank">#Isabelle</a> <a class="hashtag" href="https://agda.club/tag/usability" rel="nofollow noopener noreferrer" target="_blank">#Usability</a> <a class="hashtag" href="https://agda.club/tag/theoremprovers" rel="nofollow noopener noreferrer" target="_blank">#TheoremProvers</a>

blake shaw 🇵🇸"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way." - Jacob Lurie<a href="https://www.youtube.com/watch?v=eNgUQlpc1m0" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.youtube.com/watch?v=eNgUQlpc1m0</a><a href="https://functional.cafe/tags/theoremprovers" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#theoremprovers</a> <a href="https://functional.cafe/tags/coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#coq</a> <a href="https://functional.cafe/tags/agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#agda</a> <a href="https://functional.cafe/tags/lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lean</a> <a href="https://functional.cafe/tags/mathematics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#mathematics</a> <a href="https://functional.cafe/tags/hott" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#hott</a>

Recherches récentes

Options de recherche

Administré par :

Statistiques du serveur :

#theoremprovers