InfoQ<p>Introducing <a href="https://techhub.social/tags/DeepSeekProverV2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DeepSeekProverV2</span></a> - a new <a href="https://techhub.social/tags/opensource" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>opensource</span></a> <a href="https://techhub.social/tags/LLM" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLM</span></a> designed for formal theorem proving in Lean 4.</p><p>The model builds on a recursive <a href="https://techhub.social/tags/TheoremProving" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TheoremProving</span></a> pipeline powered by the company's DeepSeek-V3 foundation model.</p><p>Learn more: <a href="https://bit.ly/3ZlTt7h" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">bit.ly/3ZlTt7h</span><span class="invisible"></span></a> </p><p><a href="https://techhub.social/tags/InfoQ" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>InfoQ</span></a> <a href="https://techhub.social/tags/GenerativeAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>GenerativeAI</span></a></p>
Recent searches
No recent searches
Search options
Only available when logged in.
eupolicy.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
This Mastodon server is a friendly and respectful discussion space for people working in areas related to EU policy. When you request to create an account, please tell us something about you.
Administered by:
Server stats:
214active users
eupolicy.social: About · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.3.8
#TheoremProving
0 posts · 0 participants · 0 posts today
Volker Stolz<p>Channeling some PhD vacancies from our 🇳🇱 friends:</p><p>Six fully-funded PhD positions (4 years) in the project "Cyclic Structures in Programs and Proofs – New Harmonies in Software Correctness by Construction"</p><p>Deadline: Friday, May 23, 2025</p><p><a href="https://cyclic-structures.gitlab.io/vacancies/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cyclic-structures.gitlab.io/va</span><span class="invisible">cancies/</span></a></p><p><a href="https://mastodon.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalMethods</span></a> <a href="https://mastodon.social/tags/TheoremProving" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TheoremProving</span></a> <a href="https://mastodon.social/tags/NWOnl" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>NWOnl</span></a></p>
Tom de Jong<p>Call for Papers<br>16th International Conference on Interactive Theorem Proving — ITP'25</p><p>Reykjavik, Iceland<br>27 September – 3 October 2025</p><p><a href="https://icetcs.github.io/frocos-itp-tableaux25/itp/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">icetcs.github.io/frocos-itp-ta</span><span class="invisible">bleaux25/itp/</span></a></p><p>ITP is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.</p><p>- Abstract submission deadline: 12 March 2025<br>- Paper submission deadline: 19 March 2025<br>- Author notification: 23 May 2025<br>- Camera-ready copy due: 27 June 2025</p><p><a href="https://mathstodon.xyz/tags/formalization" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalization</span></a> <a href="https://mathstodon.xyz/tags/theoremproving" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>theoremproving</span></a> <a href="https://mathstodon.xyz/tags/proofassistants" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>proofassistants</span></a> <a href="https://mathstodon.xyz/tags/verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>verification</span></a> <a href="https://mathstodon.xyz/tags/CfP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CfP</span></a></p>
Jesper Agdakx 🔸<p>The pre-print for the <a class="hashtag" href="https://agda.club/tag/icpc" rel="nofollow noopener noreferrer" target="_blank">#ICPC</a> paper “Pinpointing the Learning Obstacles of an Interactive Theorem Prover” by <span class="h-card"><a class="u-url mention" href="https://mastodon.social/@sarantja" rel="nofollow noopener noreferrer" target="_blank">@<span>sarantja</span></a></span> <span class="h-card"><a class="u-url mention" href="https://mastodon.social/@azaidman" rel="nofollow noopener noreferrer" target="_blank">@<span>azaidman</span></a></span> and yt is now available at <a href="https://sarajuhosova.com/assets/files/2025-icpc.pdf" rel="nofollow noopener noreferrer" target="_blank">https://sarajuhosova.com/assets/files/2025-icpc.pdf</a></p><p>I very much hope this will inspire more research on the usability and accessibility of the languages we build going forward!</p><p>Abstract:</p><blockquote><p>Interactive theorem provers (ITPs) are programming languages which allow users to reason about and verify their programs. Although they promise strong correctness guarantees and expressive type annotations which can act as code summaries, they tend to have a steep learning curve and poor usability. Unfortunately, there is only a vague understanding of the underlying causes for these problems within the research community. To pinpoint the exact usability bottlenecks of ITPs, we conducted an online survey among 41 computer science bachelor students, asking them to reflect on the experience of learning to use the Agda ITP and to list the obstacles they faced during the process. Qualitative analysis of the responses revealed confusion among the participants about the role of ITPs within software development processes as well as design choices and tool deficiencies which do not provide an adequate level of support to ITP users. To make ITPs more accessible to new users, we recommend that ITP designers look beyond the language itself and also consider its wider contexts of tooling, developer environments, and larger software development processes. </p></blockquote><p><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/theoremproving" rel="nofollow noopener noreferrer" target="_blank">#TheoremProving</a> <a class="hashtag" href="https://agda.club/tag/dependenttypes" rel="nofollow noopener noreferrer" target="_blank">#DependentTypes</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/accessibility" rel="nofollow noopener noreferrer" target="_blank">#Accessibility</a> <a class="hashtag" href="https://agda.club/tag/icpc25" rel="nofollow noopener noreferrer" target="_blank">#ICPC25</a></p>
ExploreLive feeds
Mastodon is the best way to keep up with what's happening.
Follow anyone across the fediverse and see it all in chronological order. No algorithms, ads, or clickbait in sight.
Create accountLoginDrag & drop to upload