Mario Carneiro
41 followers
41 followers
Mario's posts
Post has attachment
Dirichlet's theorem
There have been some calls for an informal exposition of the recent formal proof of Dirichlet's theorem: Theorem 9.4.1 ( dirith , Dirichlet's theorem): If $N\in\Bbb N$ and $(A,N)=1$, then there are infinitely many primes $p$ such that $N\mid p-A$. If you ha...﻿
Post has attachment
Mathbox update: Functions of Number Theory
I should probably apologize for having nothing but mathbox updates on this blog of late, but this is the only type of post I release regularly, in conjunction with the actual theorems being uploaded to the Metamath site. (I try to make up for it by making f...﻿
Post has attachment
Mathbox update: Fundamental Theorem of Algebra
The main theorems in this short update are Van der Waerden's theorem (already discussed in a previous post ) and the Fundamental Theorem of Algebra. This last one is one of the metamath 100, and the proof was surprisingly straightforward. The hardest part w...﻿
Post has attachment
Mathbox update: Ostrowski's theorem
Hello all, This update has two main foci: the rounding off of the integration theorems with the integration by parts and integration by substitution formulas, and an unrelated work to formalize the concept of an absolute value over a ring (in the algebra se...﻿
Post has attachment
Mathbox update: The Fundamental Theorem of Calculus
Today I just put the finishing touches on a proof of the Fundamental Theorem of Calculus, which is the first theorem from the Formalizing 100 Theorems list to be proven since the creation of this blog, and has been the main reason for my recent fixation on ...﻿
Post has attachment
Integral of a positive function is positive
Here is a nice theorem that is not as simple as the statement would have you believe: Theorem ( itggt0 ): If $f$ is integrable and $A$ is a measurable set such that $0<\DeclareMathOperator{\vol}{vol}\vol(A)\le\infty$ and $f(x)>0$ for all $x\in A$, then \$\in...﻿
Post has attachment
Van der Waerden's theorem
To take a break from all this real analysis, I thought I'd change gears and formalize a gem of number theory, which goes by the name of Van der Waerden's theorem . The proof is not yet complete, so instead I'll just lay out the high-level strategy of the pr...﻿
Post has attachment
Mathbox update: More integrals
This is the first post on this blog in the mathbox-update category, so allow me to explain what this is. I periodically release my latest work in Metamath to the database, and in this post I go over the highlights and additions to be found in the release, l...﻿