José A. Alonso

Mathematician interested in the study and teaching of computational logic, functional programming and interactive theorem proving.

Public Key

npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw

NIP-05 Address

Jose_A_Alonso_at_mathstodon.xyz@mostr.pub

Profile Code

nprofile1qqsqa7mmeyplf3n3dn2dq7ps6dzd02l9kcr6z4k78n0p4sd9hu32u8q5nqtll

Author Public Key

npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pw

Show more details

Last Notes

2025-04-05 17:56:48

Demostraciones con Lean4 y con Isabelle/HOL de "f(s ∪ t) = f(s) ∪ f(t)". https://jaalonso.github.io/calculemus/posts/2021/06/06-imagen_de_la_union/ #LeanProver #IsabelleHOL #Math #Calculemus

2024-12-19 15:17:55

A formalization of sequent calculus for classical implicational logic. ~ Frederik Krogsdal Jacobsen, Jørgen Villadsen. https://backend.orbit.dtu.dk/ws/portalfiles/portal/383716082/Isabelle_2024_paper_5.pdf #ITP #IsabelleHOL #Logic

2024-10-23 06:57:28

Confirmado el descubrimiento del primo de Mersenne número 52. https://www.gaussianos.com/confirmado-el-descubrimiento-del-primo-de-mersenne-numero-52/ ~ Miguel Ángel Morales (@npub1z2f…4f6e). #Matemáticas

2024-10-23 06:55:14

Lean: First steps (Appendix A - Taxonomy). ~ Tariq Rashid (@npub10p4…jn3m). https://leanfirststeps.blogspot.com/2024/10/appendix-taxonomy.html #ITP #Lean4 #Math

2024-10-23 06:55:08

"La máxima especialización equivale a la máxima incultura." ~ José Ortega y Gasset (1883-1955). #Filosofía

2024-10-08 12:21:34

Using Org Mode to write and organize a book. ~ Ron Galloway. https://static1.squarespace.com/static/661587048ee66c27f27eecc8/t/66b9334e115dc60c33c31152/1723413327084/orgmode_guide.pdf #Emacs #OrgMode

2024-10-08 11:56:03

Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. ~ Karol Pąk, Cezary Kaliszyk. https://arxiv.org/abs/2410.00065 #ITP #Mizar #Math

2024-09-26 05:50:58

Readings shared September 25, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/25-readings_shared_09-25-24 #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #FunctionalProgramming

2024-09-11 15:26:54

ATPs as universal AIs: What do AGI architectures suggest for ATP research? ~ Zarathustra Goertzel. https://aitp-conference.org/2024/slides/ZG.pdf #ATP #AI

2024-09-11 15:18:10

Isabelle/RL project proposal: Reinforcement learning on the Isabelle proof assistant. ~ Jonathan Julián Huerta y Munive. https://aitp-conference.org/2024/slides/JJHM.pdf #ITP #IsabelleHOL #MachineLearning

2024-09-07 11:17:38

Metaprogramming in Lean. ~ Siddhartha Gadgil. https://youtube.com/playlist?list=PL_bVGic_CrGtMw1QVFRLRsZjcymm56mRi&si=xCh3BrJr1Dgq_xSE #ITP #LeanProver #Lean4

2024-08-26 06:01:04

Game programming in Prolog (Part 1). ~ Youngjin Kang. https://thingspool.net/morsels/page-10.html #Prolog #LogicProgramming

2024-08-26 05:47:30

A formalized programming language with speculative execution. ~ Jamie Wright & Andrei Popescu. https://www.isa-afp.org/entries/IMP_With_Speculation.html #ITP #IsabelleHOL

2024-08-25 09:30:12

#MULCIA: 4y PhD in Logic - the Computational Data Analytics group of Johannes Fürnkranz, JKU Linz (Austria). https://tinyurl.com/33fcnajr #PhD #CompSci

2024-08-25 09:26:54

#MULCIA: funded PhD Studentship in Proof-theoretic Semantics, UCL (Londen, UK). https://tinyurl.com/mp764tsk #PhD #CompSci

2024-08-25 09:23:18

#MULCIA: 4y PhD/Postdoc Project TAIGER: Training and Guiding AI Agents with Ethical Rules, TU Wien (Austria). https://tinyurl.com/4r84jcpd #PhD #PostDoc #CompSci

2024-08-25 07:38:45

Readings shared August 24, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/25-readings_shared_08-24-24 #Logic #Racket #ITP #Coq #Agda #TypeTheory #CurryHoward

2024-08-24 07:35:41

Logic and computation intertwined. ~ Prabhakar Ragde. https://cs.uwaterloo.ca/~plragde/flaneries/LACI/ #Logic #Racket #ITP #Coq #Agda

2024-08-24 07:27:43

Tipos dependientes: λP. ~ Juan Pablo Yamamoto Zazueta. https://jpyamamoto.com/projects/dependent-types/dept.pdf #TypeTheory #CurryHoward

2024-08-24 07:15:55

Readings shared August 23, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/24-readings_shared_08-23-24 #ITP #IsabelleHOL #LeanProver #Lean4 #AI #DeepLearning #Haskell #FunctionalProgramming #LogicProgramming #Python

2024-08-20 11:47:45

Improving on AlphaProof: IMO 2024 problem 2 in Lean 4. ~ David Renshaw. https://youtu.be/5IARsdn78xE #ITP #Lean4 #Math #AlphaProof

2024-08-20 09:47:40

An introduction to categorical proof theory. ~ Amirhossein Akbar Tabatabai. https://arxiv.org/abs/2408.09488 #Logic #Math #CategoryTheory #TypeTheory

2024-08-20 09:35:31

Beyond trees: Calculating graph-based compilers (Functional pearl). ~ Patrick Bahr & Graham Hutton. https://dl.acm.org/doi/pdf/10.1145/3674638 #Haskell #FunctionalProgramming

2024-08-20 09:32:31

Refinement composition logic. ~ Youngju Song & Dongjae Lee. https://dl.acm.org/doi/pdf/10.1145/3674645 #ITP #Coq

2024-08-20 09:31:09

Snapshoble stores. ~ Clément Allain, Basile Clément, Alexandre Moine & Gabriel Scherer. https://dl.acm.org/doi/pdf/10.1145/3674637 #ITP #Coq

2024-08-20 09:29:17

A two-phase infinite/finite low-level memory model (Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction). ~ Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski & Steve Zdancewic. https://dl.acm.org/doi/pdf/10.1145/3674652 #ITP #Coq

2024-08-20 09:27:01

Verification and attack synthesis for network protocols. ~ Max von Hippel. https://repository.library.northeastern.edu/files/neu:ms35v299k/fulltext.pdf #ITP #ACL2

2024-08-20 09:20:23

Readings shared August 18, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/20-readings_shared_08-19-24/ #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Calculemus

2024-08-19 10:18:26

Proofs of the equivalence of reverse definitions in Lean4 and Isabelle/HOL. https://jaalonso.github.io/calculemus/posts/2024/08/19-equivalence_of_reverse_definitions/ #ITP #Lean4 #IsabelleHOL #Math #Calculemus

2024-08-19 10:13:08

Proofs of the equivalence of inverse definitions in Lean4 and Isabelle/HOL. https://jaalonso.github.io/calculemus/posts/2024/08/19-equivalence_proofs_of_inverse_definitions/ #ITP #Lean4 #IsabelleHOL #Math #Calculemus

2024-08-19 06:14:01

A formalisation of the Mathieu-24 group. ~ Edward van de Meent. https://studenttheses.uu.nl/bitstream/handle/20.500.12932/47248/Bachelor_thesis%20(4).pdf #ITP #LeanProver #Lean4 #Math

2024-08-19 05:51:46

Readings shared August 18, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/19-readings_shared_08-18-24/ #ITP #LeanProver #Lean4 #FunctionalProgramming #Math #Prolog #LogicProgramming

2024-08-18 10:25:57

Lean again. ~ Adolfo Neto (@npub1gvl…8hce). https://youtu.be/ywBsvy4MxSc #ITP #Lean4 #FunctionalProgramming

2024-08-18 07:29:48

How the Lean language brings math to coding and coding to math. ~ Leo de Moura. https://www.amazon.science/blog/how-the-lean-language-brings-math-to-coding-and-coding-to-math #ITP #LeanProver #Math

2024-08-18 07:11:08

The semantics of metapropramming in Prolog. ~ David S. Warren. https://arxiv.org/abs/2408.07652 #Prolog #LogicProgramming

2024-08-18 06:58:54

Readings shared August 17, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/18-readings_shared_08-17-24/ #ITP #LeanProver #Lean4 #Math #AI

2024-08-16 15:16:59

Machine-checked proofs and the rise of formal methods in mathematics. ~ Leonardo de Moura. https://www.youtube.com/live/ekYeqvMcaWQ #ITP #LeanProver #Math

2024-08-16 14:38:20

DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. ~ Huajian Xin et als. https://www.arxiv.org/abs/2408.08152 #ITP #Lean4

2024-08-16 14:38:16

The AI scientist: Towards fully automated open-ended scientific discovery. ~ Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune & David Ha. https://arxiv.org/abs/2408.06292 #AI

2024-08-16 11:50:17

Readings shared August 15, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/16-readings_shared_08-15-24/ #ITP #IsabelleHOL #Coq #SSReflect #Math #Haskell #Elm #FunctionalProgramming

2024-08-15 17:03:37

Galois theory. ~ Tom Leinster. https://arxiv.org/abs/2408.07499 #Math

2024-08-15 17:00:16

The Haskell Unfolder Episode 31: nothunks. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@npub1e06…8ujd). https://www.youtube.com/live/NTW62s3mrXQ #Haskell #FunctionalProgramming

2024-08-15 16:48:23

Functional algorithms verified in SSReflect. ~ Alex Gryzlov et als. https://github.com/clayrat/fav-ssr/ #ITP #Coq #SSReflect

2024-08-15 16:37:53

Haskell for Elm developers: giving names to stuff (Part 5 - Semigroups and Monoids). ~ Flavio Corpa (@FlavioCorpa). https://flaviocorpa.com/haskell-for-elm-developers-giving-names-to-stuff-part-5-semigroups-and-monoids.html #Haskell #Elm #FunctionalProgramming

2024-08-15 12:38:56

Software verification with Isabelle/HOL. ~ Peter Höfner. https://comp.anu.edu.au/courses/comp4011-itp/lectures/comp4011_slides.pdf #ITP #IsabelleHOL

2024-08-15 12:29:55

Readings shared August 14, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/15-readings_shared_08-14-24/ #ITP #LeanProver #Lean4 #IsabelleHOL #Math #AI #MachineLearning

2024-08-14 15:22:07

Taller de Lean 4. Enric Cosme, Mario Vago. https://www.uv.es/coslloen/Lean4.html #ITP #LeanProver #Lean4

2024-08-14 14:53:51

Introduction to Proofs with Lean Proof Assistant. ~ Sina Hazratpour (@sina_htpr). https://sinhp.github.io/teaching/2022-introduction-to-proofs-with-Lean #ITP #LeanProver

2024-08-14 14:43:48

#Calculemus: Proofs with Lean4 and Isabelle/HOL of "take n xs ++ drop n xs = xs". https://jaalonso.github.io/calculemus/posts/2024/08/14-proofs_of_take_n_xs_%2B%2B_drop_n_xs_eq_xs/ #ITP #Lean4 #IsabelleHOL #Math

2024-08-14 10:00:33

#MULCIA: Research Assistant/Research Associate in Systems Software Verification. https://www.jobs.cam.ac.uk/job/47870/ #PostDoc #CompSci

2024-08-14 09:31:49

Readings Shared August 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/14-lecturas_compartidas_el_13-ago-24 #ITP #Coq #Agda #Math #Python

2024-08-14 09:03:10

Lecturas compartidas el 13 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/14-lecturas_compartidas_el_13-ago-24 #ITP #Coq #Agda #Math #Python

2024-08-13 09:43:44

Sharing proofs with predicative theories through universe-polymorphic elaboration. ~ Thiago Felicissimo & Frédéric Blanqui. https://arxiv.org/abs/2308.15465 #ITP #Agda #Coq

2024-08-13 09:42:14

An elementary proof of the FMP for Kleene algebra. ~ Tobias Kappé. https://arxiv.org/abs/2212.10931 #ITP #Coq #Math

2024-08-13 09:40:16

Bounding Euler's constant. ~ Philip Zucker (@npub1sxl…75kj). https://www.philipzucker.com/knuck_exp/ #Math #Python

2024-08-13 09:33:07

Algebra. It's powerful. But it's not what it was. ~ Keith Devlin (@npub1czu…fcwe). https://www.mathvalues.org/masterblog/algebra-its-not-what-it-was #Math

2024-08-12 16:39:12

MathPartner (will help you to solve mathematical problems). https://mathpar.com/en/welcome.html #Math #CAS #MathParner

2024-08-12 16:18:57

MathPartner: An artificial intelligence cloud service. ~ Gennadi Malaschonok & Alexandr Seliverstov. https://arxiv.org/abs/2408.04999 #Math #CAS #MathParner

2024-08-11 10:39:11

Lecturas compartidas el 10 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/11-lecturas_compartidas_el_10-ago-24 #Python #Haskell #FunctionalProgramming

2024-08-10 16:37:56

Function composition and currying in Python (Python in the streets, Haskell in the sheets!). ~ Francisco Gutierrez. https://freefrancisco.hashnode.dev/function-composition-and-currying-in-python #Python #Haskell #FunctionalProgramming

2024-08-10 11:55:44

Lecturas compartidas el 9 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/10-lecturas_compartidas_el_09-ago-24 #ITP #IsabelleHOL #LeanProver #HOL4 #Coq #Math #Haskell #FunctionalProgramming #IA

2024-08-09 17:48:27

#MULCIA: Postdoc Position in AI for Mathematics at Meta FAIR. https://tinyurl.com/55mzvm86 #PostDoc #CompSci #AI

2024-08-09 17:42:35

#MULCIA: PostDoc on Lean + Compilers at the University of Cambridge https://tinyurl.com/mr3r773h #PostDoc #CompSci #LeanProver

2024-08-09 17:27:20

Competitive programming in Haskell: Tree path decomposition, part II. ~ Brent Yorgey (@npub1wrp…97pa). https://byorgey.github.io/blog/posts/2024/08/08/TreeDecomposition.html #Haskell #FunctionalProgramming

2024-08-09 17:23:35

Formalising the double-pushout approach to graph transformation. ~ Robert Söldner & Detlef Plump. https://arxiv.org/abs/2312.15641 #ITP #IsabelleHOL

2024-08-09 17:20:23

First steps towards computational polynomials in Lean. ~ James Harold Davenport. https://arxiv.org/abs/2408.04564 #ITP #LeanProver #Math

2024-08-09 17:15:28

An in-context learning agent for formal theorem-proving. ~ Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin & Swarat Chaudhuri. https://arxiv.org/abs/2310.04353 #LLMs #ITP #Coq #LeanProver

2024-08-09 17:04:38

The potential for AI in science and mathematics. ~ Terence Tao. https://youtu.be/_sTDSO74D8Q #IA #Math #ITP #LeanProver

2024-08-09 16:57:50

A tricky lower bound proof. ~ Lawrence Paulson (@npub12ku…yaeg). https://lawrencecpaulson.github.io/2024/08/08/Ln_lower_bound.html #ITP #IsabelleHOL #Math

2024-08-09 15:58:48

Intelligent Computer Mathematics (17th International Conference, CICM 2024, Proceedings). https://books.google.nl/books?id=Y7IXEQAAQBAJ&lpg=PP1&hl=es&pg=PP1#v=onepage&q&f=false #ITP #Math

2024-08-09 15:42:19

Validation of HOL4's formal floating-point model. ~ Hugo Eidmann. https://www.diva-portal.org/smash/get/diva2:1879248/FULLTEXT01.pdf #ITP #HOL4

2024-08-09 15:37:08

Verified transformations for convex programming. ~ Ramon Fernández Mir. https://era.ed.ac.uk/bitstream/handle/1842/42057/Fern%C3%A1ndez%20Mir2024.pdf #ITP #Lean4 #Math

2024-08-09 15:32:38

Validation of a formal floating-point model for the interactive proof assistant Isabelle/HOL. ~ Olof Lindström. https://www.diva-portal.org/smash/get/diva2:1879891/FULLTEXT01.pdf #ITP #IsabelleHOL

2024-08-09 15:20:39

typedKanren: Statically typed relational programming with exhaustive matching in Haskell. ~ Nikolai Kudasov & Artem Starikov. https://arxiv.org/abs/2408.03170 #Haskell #FunctionalProgramming

2024-08-09 15:14:05

Combinatorial and algorithmic mathematics (From foundation to optimization) ~ Baha M. Alzalg. https://books.google.nl/books?id=_6eJEAAAQBAJ&lpg=PR1&hl=es&pg=PR8#v=onepage&q&f=false #Math

2024-08-09 12:05:06

Lecturas compartidas el 8 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/09-lecturas_compartidas_el_08-ago-24 #ITP #Lean4 #IsabelleHOL #Math #DeepLearning

2024-08-07 11:47:28

#Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "length(xs ++ ys) = length(xs) + length(ys)". https://jaalonso.github.io/calculemus/posts/2024/08/07-pruebas_de_lengthxs_%2B%2B_ys_ig_length_xs%2Blength_ys/ #ITP #Lean4 #IsabelleHOL #Math

2024-08-07 09:43:25

Getting started with Blueprint-Driven formalization projects in Lean. ~ Pietro Monticone (@npub1qjt…t3lu). https://youtu.be/KyuyTsLgkMY #ITP #LeanProver #Lean4

2024-08-07 07:03:50

A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si. https://arxiv.org/abs/2404.09939 #ITP #DeepLearning

2024-08-07 06:46:21

Lecturas compartidas el 6 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/07-lecturas_compartidas_el_06-ago-24 #ITP #Coq #Python #FunctionalProgramming

2024-08-06 11:42:02

Functional programming in Python: When and how to use it. ~ John Sturtz. https://realpython.com/python-functional-programming/ #Python #FunctionalProgramming

2024-08-06 11:27:55

Rely-guarantee semantics for separation-logic-based specification extraction. ~ Paul He. https://paulhe.com/assets/thesis.pdf #PhDThesis #ITP #Coq

2024-08-06 11:20:51

Lecturas compartidas el 5 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/06-lecturas_compartidas_el_05-ago-24 #ATP #SAT #Haskell #FunctionalProgramming #CurryHoward #TypeScript

2024-08-05 07:14:52

Proofs are programs: A few examples of the Curry-Howard correspondence. ~ Adam Dueck. https://adueck.github.io/blog/curry-howard-proofs-are-programs/ #CurryHoward #TypeScript

2024-08-05 07:11:52

Why does everyone hate Haskell, jazz, and pure math? ~ Adam Dueck. https://adueck.github.io/blog/on-haskell-jazz-and-pure-math/ #Haskell #FunctionalProgramming

2024-08-05 06:55:26

A SAT-based approach to rigorous verification of Bayesian networks. ~ Ignacy Stępka, Nicholas Gisolfi & Artur Dubrawski. https://arxiv.org/abs/2408.00986 #ATP #SAT

2024-08-05 06:44:34

Lecturas compartidas el 4 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/05-lecturas_compartidas_el_04-ago-24 #ITP #IsabelleHOL #Diproche #Math

2024-08-04 10:53:12

Sociomathematical norms and automated proof checking in mathematical education: Reflections and experiences. ~ Merlin Carl. https://scholarship.claremont.edu/cgi/viewcontent.cgi?article=1991&context=jhm #ITP #Diproche #Math

2024-08-04 10:47:47

The top-down solver verified: Building confidence in static analyzers. Yannick Stade, Sarah Tilscher & Helmut Seidl. https://link.springer.com/chapter/10.1007/978-3-031-65627-9_15 #ITP #IsabelleHOL

2024-08-04 10:37:56

Lecturas compartidas el 3 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/04-lecturas_compartidas_el_03-ago-24 #Math

2024-08-03 08:40:50

Lecturas compartidas el 2 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/03-lecturas_compartidas_el_02-ago-24 #ITP #LeanProver #IsabelleHOL #Coq #MinLog #Agda #Logic #Math #FunctionalProgramming #Haskell #Hope #Miranda

2024-08-02 15:32:22

Data.Maybe, and thoughts on library design. ~ Srijan Paul (@_injuly). https://injuly.in/blog/monoid-maybe #Haskell #FunctionalProgramming

2024-08-02 15:29:55

Analyzing Haskell stability. ~ Jappie Klooster (@jappieklooster). https://jappie.me/analyzing-haskell-stability.html #Haskell #FunctionalProgramming

2024-08-02 15:27:06

Where does the name "algebraic data type" come from? ~ Li-yao Xia (@lysxia). https://blog.poisson.chat/posts/2024-07-26-adt-history.html #FunctionalProgramming #Hope #Miranda

2024-08-02 12:44:58

Inteligencia Artificial y capital humano: ¿Pueden estar en peligro sus complementariedades? ~ Juan F. Jimeno y Ana Lamo. https://www.funcas.es/wp-content/uploads/2024/07/PEE-180-WEB1.pdf#page=103 #IA

2024-08-02 12:32:53

La demanda de educación superior ante el cambio tecnológico y la inteligencia artificial. ~ José Ignacio Conde-Ruiz, Juan José Ganuza, Manu García y Carlos Victoria. https://www.funcas.es/wp-content/uploads/2024/07/PEE-180-WEB1.pdf#page=76 #IA #Educación

2024-08-02 12:28:38

Esta vez sí: Con la IA, nada será igual en la Universidad. ~ Mariano Fernández Enguita. https://www.funcas.es/wp-content/uploads/2024/07/PEE-180-WEB1.pdf#page=35 #IA #Educación

2024-08-02 12:05:40

Semantical analysis of intuitionistic modal logics between CK and IK. ~ Jim de Groot, Ian Shillito & Ranald Clouston. https://arxiv.org/abs/2408.00262 #ITP #Coq #Logic

2024-08-02 12:02:29

Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis. ~ Grigory Devadze, Victor Magron & Stefan Streif. https://arxiv.org/abs/2006.09884 #ITP #MinLog #Math

2024-08-02 10:48:20

Semialgebraic groups and generalized affine buildings. ~ Raphael Appenzeller. https://arxiv.org/abs/2407.20406# #PhDThesis #ITP #LeanProver #Math