#theoremproving — Public Fediverse posts

Want to learn more about the latest developments on using AI and (interactive) theorem proving in Mathematics? Wait no longer!

We have a great line-up of speakers at our online Workshop on AI and Theorem Provers in Mathematics. The workshop will be held online from 8th to 10th of April and attendance is free (registration required). For more details, visit the workshop website: https://aitpm.github.io/

#math #itp #theoremProving #isabelleHOL #lean #llm #ai #formal_mehods #agda #hol #mathematics

Emily Riehl: How I became seduced by Univalent Foundations

[tbh I think shes only disclosing her theoretical motivations her; I recall she was posting questions about Linux distros a few years ago, and if we're honest being a nerd is the actual reason 99% of people get into HoTT]
https://www.youtube.com/watch?v=XIYoI5j5Flo&t=486s

#hott #mathematics #categorytheory #theoremproving

#CondensedDetachment example

Axiom 1: ⊢ (𝜑 → (𝜓 → 𝜑))
Axiom 2: ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Rule of Modus Ponens:
• Major hypothesis: ⊢ (𝜓 → 𝜑)
• Minor hypothesis: ⊢ 𝜓
• Resulting Assertion: ⊢ 𝜑
——
D<major><minor> applies the Rule of Modus Ponens treating the two given tautologies as having metavariables living in different namespaces and returning the normalized result. We extend by using underscore as a placeholder, so D__ recovers the rule of modus ponens.
——
"D2_" is proof of the rule:
• Hypothesis: ⊢ (𝜑 → (𝜓 → 𝜒))
• Resulting assertion: ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
——
"D21" is a proof which unifies "1" ⊢ (𝜑′ → (𝜓′ → 𝜑′)) with the hypothesis of "D2_" giving the substitution map 𝜎: {𝜑′ ↦ 𝜑, 𝜓′ ↦ 𝜓, 𝜒 ↦ 𝜑} resulting in the tautology: ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜑))

(Note that unification can map variables from either side, but when faced with a variable matching a term has to match the variable to that term.)
——
"DD21_" is proof of the rule:
• Hypothesis: ⊢ (𝜑 → 𝜓)
• Resulting assertion: ⊢ ((𝜑 → 𝜑)
——
"DD211" is a proof which unifies "1" ⊢ (𝜑″ → (𝜓″ → 𝜑″)) with the hypothesis of "DD21_" giving the substitution map 𝜎: {𝜑″ ↦ 𝜑, 𝜓 ↦ (𝜓″ → 𝜑)} resulting in the tautology: ⊢ (𝜑 → 𝜑)

This has been adapted and expanded from a run of my symbolic-mgu pre-release crate. https://crates.io/crates/symbolic-mgu

cargo run -r --bin compact -- --wide D__ 1 2 D2_ D21 DD21_ DD211

#math #logic #theoremProving #rust #mostGeneralUnifier #mgu

An abbreviated run for examining sub-proofs of propositional logic from Russell and Whitehead, and proving that they are all tautologies:

```
% cargo test --features serde,bigint -r --test pmproofs_validation -- --include-ignored --no-capture

running 1 test
Validating PM subproofs...
Variable limit: unlimited (bigint feature enabled)
Total subproofs in database: 2997
Processed 100/2997 subproofs...
Processed 200/2997 subproofs...

...

Processed 2800/2997 subproofs...
Processed 2900/2997 subproofs...

========================================
PM SUBPROOF VALIDATION RESULTS
========================================
Total subproofs: 2997
Parse failures: 0
Skipped (too many variables): 0
Validation errors: 0
Not tautologies: 0
Successfully validated: 2997

✓ Successfully validated 2997 subproofs!
test all_pm_subproofs_are_tautologies ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 2.60s

```

#Rust #logic #math #theoremProving #condensedDetachment #mostGeneralUnifier #mgu

I'm writing an open source math library in #Rust to do symbolic unification. (following Meredith, Robinson, Megill) It's in pre-release (v0.1.0-alpha.13) now but I'm nearly feature-complete and I'm beginning to write interesting demonstrations with it.

I thought now would be a time to solicit feedback before the API stabilizes as per semantic versioning best practices.

Like many compilers built on top of the LLVM architecture, un-optimized Rust is about 10 times slower than the optimized code produced with the --release flag. You can really notice this with the test that sets out to exhaustively produce all expressions on sets of limited operators until all 16 Boolean functions are produced. https://docs.rs/crate/symbolic-mgu/latest/source/tests/functional_completeness.rs

Also I run through Norm Megill's archive of shortest known proofs of propositional logic statements from Whitehead and Russell's Prinicipia Mathematica and test that they and all subproofs produce tautologies. https://docs.rs/crate/symbolic-mgu/latest/source/tests/pmproofs_validation.rs

Documentation: https://docs.rs/symbolic-mgu/latest/symbolic_mgu/
Distribution: https://crates.io/crates/symbolic-mgu
Repository: https://github.com/arpie-steele/symbolic-mgu

#logic #theoremProving #condensedDetachment #mostGeneralUnifier #mgu #math

We're thrilled to welcome Alexander Bentkamp to the Cryspen family!

Alex joins our Tools and Proofs team with a deep background in automated and interactive theorem proving, especially with the Lean proof assistant. We're excited to have his expertise as we continue our work on formally verifying security-critical software.

Welcome aboard, Alex!

https://cryspen.com/post/welcome_alex/

#Cryspen #Welcome #FormalVerification #TheoremProving

DeepSeek Releases Massive 671B Prover V2 Model For Mathematical Theorem Proving Ahead of R2 Release

#AI #ChinaAI #DeepSeek #OpenSourceAI #Math #TheoremProving #Lean4 #MachineLearning #DeepLearning #MathAI

https://winbuzzer.com/2025/04/30/deepseek-releases-massive-671b-prover-v2-model-for-mathematical-theorem-proving-ahead-of-r2-release-xcxwbn/

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

#formalization #theoremproving #proofassistants #verification #CfP

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.

#Agda #TheoremProving #DependentTypes #Usability #Accessibility #ICPC25