Capturing properties of planar diagrams in Lean proof assistant software
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911436191563776 |
|---|---|
| author | Litterick, Alastair Vernitski, Alexei Woods, Billy |
| author_facet | Litterick, Alastair Vernitski, Alexei Woods, Billy |
| contents | Automated proof assistants are a technology pre-empting mistakes in mathematics. In our practice we have seen that reasoning about planar diagrams is difficult to both humans and computers. One example that has led to wrong statements in publications is that an orientation-preserving mapping is not always defined by how it acts on triples of elements. In this paper we formalise orientation-preserving mappings in proof assistant software Lean and report on our take-aways. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_13304 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Capturing properties of planar diagrams in Lean proof assistant software Litterick, Alastair Vernitski, Alexei Woods, Billy Combinatorics Logic in Computer Science Group Theory Automated proof assistants are a technology pre-empting mistakes in mathematics. In our practice we have seen that reasoning about planar diagrams is difficult to both humans and computers. One example that has led to wrong statements in publications is that an orientation-preserving mapping is not always defined by how it acts on triples of elements. In this paper we formalise orientation-preserving mappings in proof assistant software Lean and report on our take-aways. |
| title | Capturing properties of planar diagrams in Lean proof assistant software |
| topic | Combinatorics Logic in Computer Science Group Theory |
| url | https://arxiv.org/abs/2511.13304 |