What the gradient is doing: a Taylor expansion you can drag around, proved in core Lean, with a Lean Studio widget
-
Updated
Sep 27, 2026 - JavaScript
#
lean-studio
Here are 5 public repositories matching this topic...
Penrose diagrams in core Lean: a box is a matrix, a wire is an index, joining wires sums over it. The zig-zag, transpose, trace and sliding rules proved for every dimension and every matrix. MIT.
linear-algebra theorem-proving tenet tensor-networks string-diagrams lean4 lean-studio penrose-diagrams
-
Updated
Sep 28, 2026 - Lean
AES-256 from FIPS-197 in Lean 4: test vectors, decrypt∘encrypt = id, S-box uniformity 4 and nonlinearity 112, branch number 5, ≥25 active S-boxes in any 4 rounds. Kernel-checked, re-checked by Tenet.
cryptography aes theorem-proving aes-256 formal-verification tenet lean4 fips-197 leanviz lean-studio
-
Updated
Sep 28, 2026 - Lean
PKCS #7 / CMS signatures (RFC 5652) in core Lean: a checker proved equal to the signing rules, Lean's kernel verifying real signatures, and seven verifiers compared. MIT.
cms security cryptography theorem-proving rsa pkcs7 x509 asn1 sha256 formal-verification smime der tenet digital-signatures rfc3161 timestamping differential-testing lean4 rfc5652 lean-studio
-
Updated
Sep 28, 2026 - Lean
X.509 in core Lean: canonical DER, SHA-256 and RSA, and Lean's kernel validating a real certificate chain end to end. MIT.
-
Updated
Sep 28, 2026 - Lean
Add this topic to your repo
To associate your repository with the lean-studio topic, visit your repo's landing page and select "manage topics."