mmasdeu

Universitat Autònoma de BarcelonaBellaterra, Catalunya

Pinned Repositories

barcelonaleanseminar
Exercises done during the weekly Lean seminar
Language:Lean4 5 21
brouwerfixedpoint
Proving Brouwer's Fixed Point Theorem in Lean
Language:Lean4 4 41
btquotients
Computing with quotients of the Bruhat-Tits tree
Language:Python2 3 01
darmonpoints
Sage package to compute Darmon points
Language:Python5 3 35
fundamental
Learn basic of LEAN and prove basic results from "Fonaments" class
Language:Lean2 3 00
hilbert
Formalization of Hilbert's axioms for plane geometry in Lean
Language:Lean2 2 01
modularforms_archive
Notes on a first course on modular forms
Language:TeX2 3 01
sage_package_template
A cookiecutter for SageMath projects
Language:Python4 5 13
topologygame
Learn Lean and topology
Language:Lean21 5 42
twostage
Algorithms for proving that class-number-one real quadratic fields are 2-stage euclidean, and to find continued fraction expansions in them
Language:Python2 4 02

mmasdeu's Repositories

mmasdeu/topologygame
Learn Lean and topology
Language:Lean21 5 42
mmasdeu/darmonpoints
Sage package to compute Darmon points
Language:Python5 3 35
mmasdeu/modularforms_archive
Notes on a first course on modular forms
Language:TeX2 3 01
mmasdeu/argo
Lean Game for Argo Course 2023
Language:Lean1 2 01
mmasdeu/lean4-tactics
Overview of tactics in Lean 4 for beginners — longer version
1 1 0
mmasdeu/modularforms
Notes for Modular Forms (part of Advanced Number Theory, Master of Advanced Mathematics UAB/UB)
Language:TeX1 1 01
mmasdeu/ruleofsigns
Formalization of Descartes' rule of signs in Lean
Language:Lean1 2 03
mmasdeu/stieltjes
Formalization of Riemann-Stieltjes integral in LEAN
Language:Lean1 2 0
mmasdeu/algebralineal
Apunts d'Àlgebra Lineal
Language:JavaScript2 0
mmasdeu/arxiv-email
A bot that sends HTML-formatted daily arXiV emails
Language:Python
mmasdeu/fonaments
Seminari de Fonaments 2023/24
Language:Lean2 01
mmasdeu/formesmodulars
Apunts per tres (o quatre) xerrades
Language:CSS1 0
mmasdeu/fuzzy
Fuzzy sets
Language:Lean2 0
mmasdeu/geometry
Geometry game
Language:Lean2 0
mmasdeu/lean-nt
Formalization of number theory results in Lean
Language:Lean3 0
mmasdeu/lean4-cheatsheet
Printable (A4) overview of tactics in Lean 4 for beginners
Language:TeX1 0
mmasdeu/lean4game
Server to host lean games, UAB customizations
Language:TypeScript1 0
mmasdeu/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
Language:CSS1 0
mmasdeu/lmfdb
L-Functions and Modular Forms Database
Language:Python1 0
mmasdeu/materials_eines
Materials per l'assignatura Eines Informàtiques per les Matemàtiques
Language:Shell2 0
mmasdeu/mathlib4
The math library of Lean 4
Language:Lean1 0
mmasdeu/moodle_nbgrader
Basic scripts for Moodle integration with nbgrader, adapted to Universitat Autònoma de Barcelona - UAB
Language:Python2 0
mmasdeu/pindolafme
Lean files for talk at FME (UPC) on using Lean in teaching
Language:Lean1 0
mmasdeu/sage_binary
Binary files for Sagemath
Language:Xonsh2 0
mmasdeu/sage_sample_new
A sage project template
Language:Xonsh1 0
mmasdeu/secundaria
Xerrada "Ensenyant formalització a través de LEAN"
Language:Lean2 0
mmasdeu/slideslftcm2023
Slides for talks at Lean for the Curious Mathematician 2023
Language:JavaScript2 0
mmasdeu/staged-recipes
A place to submit conda recipes before they become fully fledged conda-forge feedstocks
Language:Python1 0
mmasdeu/teoriadegalois
Apunts pel curs Teoria de Galois a la UAB
Language:JavaScript2 0
mmasdeu/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
Language:Lean1 0