Pinned Repositories
atrpoints
Numerical verification of conjecture of Darmon on ATR points.
barcelonaleanseminar
Exercises done during the weekly Lean seminar
biysc2021-notes
brouwerfixedpoint
Proving Brouwer's Fixed Point Theorem in Lean
btquotients
Computing with quotients of the Bruhat-Tits tree
darmonpoints
Sage package to compute Darmon points
fundamental
Learn basic of LEAN and prove basic results from "Fonaments" class
modularforms
Notes on a first course on modular forms
sage_package_template
A cookiecutter for SageMath projects
topologygame
Learn Lean and topology
mmasdeu's Repositories
mmasdeu/topologygame
Learn Lean and topology
mmasdeu/darmonpoints
Sage package to compute Darmon points
mmasdeu/fundamental
Learn basic of LEAN and prove basic results from "Fonaments" class
mmasdeu/Lean-game-maker
This project converts structured Lean code into an interactive browser game.
mmasdeu/lean4-tactics
Overview of tactics in Lean 4 for beginners — longer version
mmasdeu/ruleofsigns
Formalization of Descartes' rule of signs in Lean
mmasdeu/algebralineal
Apunts d'Àlgebra Lineal
mmasdeu/argo
Lean Game for Argo Course 2023
mmasdeu/biysc2022
Proving the plane separation theorem in Lean
mmasdeu/fonaments
Seminari de Fonaments 2023/24
mmasdeu/formesmodulars
Apunts d'un curs de formes modulars
mmasdeu/fuzzy
Fuzzy sets
mmasdeu/geometry
Geometry game
mmasdeu/lean-nt
Formalization of number theory results in Lean
mmasdeu/lean4-cheatsheet
Printable (A4) overview of tactics in Lean 4 for beginners
mmasdeu/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
mmasdeu/lmfdb
L-Functions and Modular Forms Database
mmasdeu/materials_eines
Materials per l'assignatura Eines Informàtiques per les Matemàtiques
mmasdeu/mathlib4
The math library of Lean 4
mmasdeu/mmasdeu.github.io
Marc Masdeu -- GitHub portfolio
mmasdeu/moodle_nbgrader
Basic scripts for Moodle integration with nbgrader, adapted to Universitat Autònoma de Barcelona - UAB
mmasdeu/sage-binder
A SageMath-based computing environment for binder
mmasdeu/sage_binary
Binary files for Sagemath
mmasdeu/sage_sample_new
A sage project template
mmasdeu/secundaria
Xerrada "Ensenyant formalització a través de LEAN"
mmasdeu/slideslftcm2023
Slides for talks at Lean for the Curious Mathematician 2023
mmasdeu/staged-recipes
A place to submit conda recipes before they become fully fledged conda-forge feedstocks
mmasdeu/stieltjes
Formalization of Riemann-Stieltjes integral in LEAN
mmasdeu/teoriadegalois
Apunts pel curs Teoria de Galois a la UAB
mmasdeu/verbose-lean4
Natural language tactics to teach mathematics using Lean 4