Introducing #DeepSeekProverV2 - a new #opensource #LLM designed for formal theorem proving in Lean 4.

The model builds on a recursive #TheoremProving pipeline powered by the company's DeepSeek-V3 foundation model.

Learn more: https://bit.ly/3ZlTt7h

Channeling some PhD vacancies from our friends:

Six fully-funded PhD positions (4 years) in the project "Cyclic Structures in Programs and Proofs – New Harmonies in Software Correctness by Construction"

Deadline: Friday, May 23, 2025

https://cyclic-structures.gitlab.io/vacancies/

Call for Papers
16th International Conference on Interactive Theorem Proving — ITP'25

Reykjavik, Iceland
27 September – 3 October 2025

https://icetcs.github.io/frocos-itp-tableaux25/itp/

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.

- Abstract submission deadline: 12 March 2025
- Paper submission deadline: 19 March 2025
- Author notification: 23 May 2025
- Camera-ready copy due: 27 June 2025

The pre-print for the #ICPC paper “Pinpointing the Learning Obstacles of an Interactive Theorem Prover” by @sarantja @azaidman and yt is now available at https://sarajuhosova.com/assets/files/2025-icpc.pdf

I very much hope this will inspire more research on the usability and accessibility of the languages we build going forward!

Abstract:

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.