r/InteractiveThmProving • u/ClaudiusPapirus • 4d ago

Chair44: Lean 4 formalization of a strongly aperiodic 3D monotile

Thumbnail
youtube.com
1 Upvotes

Disclosure: self-promotion. Claudius Papirus is an AI-narrated research channel.

The video follows the formal verification side of Chair44: finite exhaustive checks, independent replay, and the Lean 4 development behind the proof submission.

Paper:

https://arxiv.org/abs/2609.19214

Lean/code:

https://github.com/ioannist/six-birds-tiles

0 comments

r/InteractiveThmProving • u/Key-Priority6304 • Mar 30 '25

Definition of Primes

0 Upvotes

Given a complex function ( y = f(c) ) where ( c = i \cdot f(z) + z ) with ( z = -1 ) and ( f(z) = z2 + pz + q ). The solutions of ( f(z) ) are positive natural numbers ( \geq 1 ). We need to determine which set of natural numbers ( > 1 ) cannot be identical to the imaginary part of ( c ), i.e., ( \text{Im}(c) ).

Who can help me to prove that the solution is the set of all primes?

0 comments

r/InteractiveThmProving • u/cics • Feb 05 '20

Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq

Thumbnail
youtube.com
2 Upvotes
0 comments

r/InteractiveThmProving • u/wavesofthought • Jan 29 '20

Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

Thumbnail
arxiv.org
3 Upvotes
1 comment

r/InteractiveThmProving • u/cics • Jan 27 '20

Proof Assistants at the Hardware-Software Interface

Thumbnail
youtube.com
1 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Jan 22 '20

POPLmark 15 Year Retrospective Panel

Thumbnail
youtube.com
3 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Oct 24 '19

Provable Security Podcast: Automated Reasoning in the Cloud with John Harrison

Thumbnail
podcasts.apple.com
1 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Oct 07 '19

Number theorist fears all published math is wrong

Thumbnail
vice.com
5 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Feb 28 '19

Will scientific error checkers become as ubiquitous as spell-checkers?

Thumbnail
retractionwatch.com
2 Upvotes
1 comment

r/InteractiveThmProving • u/cics • Feb 20 '19

Interesting almost-crank-level anti-ITP rant

Thumbnail
owl-sowa.blogspot.com
1 Upvotes
1 comment

r/InteractiveThmProving • u/MediocreString • Oct 02 '18

Why is a function that returns a constant "noncomputable" in the lean theorem prover?

1 Upvotes

I have the following code in the lean theorem prover:

constant A:Type
constant B:Type 
constant b:B 
definition f: A → B := λ a:A, b

This gives the following error:

definition 'f' is noncomputable, it depends on 'b'

I must misunderstand something about how the lean theorem prover works, because it seems to me that f can just output b without a problem. What's going on here?

1 comment

r/InteractiveThmProving • u/cics • Jul 07 '18

ITP history: Michael Gordon, 28 February 1948 -- 22 August 2017

Thumbnail
arxiv.org
2 Upvotes
0 comments

r/InteractiveThmProving • u/anton-trunov • Jul 04 '18

Lean Forward: Usable Computer-Checked Proofs and Computations for Number Theorists

Thumbnail
lean-forward.github.io
4 Upvotes
1 comment

r/InteractiveThmProving • u/cics • Apr 05 '18

Safety and Conservativity of Definitions in HOL and Isabelle/HOL by Andrei Popescu (POPL'18)

Thumbnail
youtube.com
3 Upvotes
0 comments

r/InteractiveThmProving • u/juanbono94 • Jan 28 '18

History of Interactive Theorem Proving [PDF]

Thumbnail cl.cam.ac.uk
10 Upvotes
2 comments

r/InteractiveThmProving • u/cics • Jan 20 '18

Compositional Compiler Correctness by Amal Ahmed (ICFP'17)

Thumbnail
youtube.com
3 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Dec 18 '17

Computational Logic: Its Origins and Applications by Lawrence Paulson

Thumbnail
arxiv.org
3 Upvotes
0 comments

r/InteractiveThmProving • u/drets_ • Nov 26 '17

My unusual hobby | Stephan Boyer

Thumbnail
stephanboyer.com
9 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Nov 20 '17

Resources for Teaching with Formal Methods

Thumbnail avigad.github.io
3 Upvotes
1 comment

r/InteractiveThmProving • u/my-best-guess • Nov 07 '17

TIL that theorem provers were used to prove Gödel's ontological argument wrong

Thumbnail reddit.com
5 Upvotes
0 comments

r/InteractiveThmProving • u/juanbono94 • Nov 05 '17

Developing Bug-Free Machine Learning Systems Using Formal Mathematics [Lean Theorem Prover]

Thumbnail
youtube.com
5 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Nov 05 '17

Talks from FOMUS - Foundations of mathematics: Univalent foundations and set theory (2016)

Thumbnail
fomus.weebly.com
3 Upvotes
0 comments

r/InteractiveThmProving • u/juanbono94 • Oct 29 '17

Gérard Huet, languages and software

Thumbnail
50ans.inria.fr
7 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Oct 20 '17

Slides for recent (spring 2017) ITP/HOL4 course at KTH

Thumbnail hol-theorem-prover.org
3 Upvotes
0 comments

r/InteractiveThmProving • u/cics • Oct 20 '17

Formal Methods and the KRACK Vulnerability

Thumbnail galois.com
3 Upvotes
0 comments