search

sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.22k stars 425 forks source link

Meta-ticket: Connections to the Lean theorem prover #34180

Open mkoeppe opened 2 years ago

mkoeppe commented 2 years ago

https://leanprover-community.github.io/index.html

CC: junyanxu.math@gmail.com

Component: interfaces

Issue created by migration from https://trac.sagemath.org/ticket/34180

mkoeppe commented 2 years ago

Description changed:

--- 
+++ 
@@ -2,6 +2,6 @@

 - https://github.com/leanprover-community/lean-client-python

-- https://github.com/leanprover-community/mathlib/blob/master/scripts/polyrith_sage.py
+- https://github.com/leanprover-community/mathlib/blob/master/scripts/polyrith_sage.py, https://github.com/leanprover-community/mathlib/blob/master/scripts/polyrith_sage_helper.py
mkoeppe commented 2 years ago

Description changed:

--- 
+++ 
@@ -4,4 +4,5 @@

 - https://github.com/leanprover-community/mathlib/blob/master/scripts/polyrith_sage.py, https://github.com/leanprover-community/mathlib/blob/master/scripts/polyrith_sage_helper.py

+- #34182 `_lean_init_` methods for some elements, parents, axioms, and categories