Close Menu
bkngpnarnaul
  • Home
  • Education
    • Biology
    • Chemistry
    • Math
    • Physics
    • Science
    • Teacher
  • E-Learning
    • Educational Technology
  • Health Education
    • Special Education
  • Higher Education
  • IELTS
  • Language Learning
  • Study Abroad

Subscribe to Updates

Please enable JavaScript in your browser to complete this form.
Loading
What's Hot

Making PD meaningful in today’s classrooms

September 2, 2025

Just 1 minute of vigorous exercise a day could add years to your life

September 2, 2025

A crowdsourced project to link up erdosproblems.com to the OEIS

September 2, 2025
Facebook X (Twitter) Instagram
Wednesday, September 3
Facebook X (Twitter) Instagram Pinterest Vimeo
bkngpnarnaul
  • Home
  • Education
    • Biology
    • Chemistry
    • Math
    • Physics
    • Science
    • Teacher
  • E-Learning
    • Educational Technology
  • Health Education
    • Special Education
  • Higher Education
  • IELTS
  • Language Learning
  • Study Abroad
bkngpnarnaul
Home»Math»A Lean companion to “Analysis I”
Math

A Lean companion to “Analysis I”

adminBy adminJune 2, 2025No Comments3 Mins Read0 Views
Share Facebook Twitter Pinterest LinkedIn Tumblr Email WhatsApp Copy Link
Follow Us
Google News Flipboard Threads
A Lean companion to “Analysis I”
Share
Facebook Twitter LinkedIn Pinterest Email Copy Link


Almost 20 years ago, I wrote a textbook in real analysis called “Analysis I“. It was intended to complement the many good available analysis textbooks out there by focusing more on foundational issues, such as the construction of the natural numbers, integers, rational numbers, and reals, as well as providing enough set theory and logic to allow students to develop proofs at high levels of rigor.

While some proof assistants such as Coq or Agda were well established when the book was written, formal verification was not on my radar at the time. However, now that I have had some experience with this subject, I realize that the content of this book is in fact very compatible with such proof assistants; in particular, the ‘naive type theory’ that I was implicitly using to do things like construct the standard number systems, dovetails well with the dependent type theory of Lean (which, among other things, has excellent support for quotient types).

I have therefore decided to launch a Lean companion to “Analysis I”, which is a “translation” of many of the definitions, theorems, and exercises of the text into Lean. In particular, this gives an alternate way to perform the exercises in the book, by instead filling in the corresponding “sorries” in the Lean code. (I do not however plan on hosting “official” solutions to the exercises in this companion; instead, feel free to create forks of the repository in which these sorries are filled in.)

Currently, the following sections of the text have been translated into Lean:

The formalization has been deliberately designed to be separate from the standard Lean math library Mathlib at some places, but reliant on it at others. For instance, Mathlib already has a standard notion of the natural numbers {{\bf N}}. In the Lean formalization, I first develop “by hand” an alternate construction Chapter2.Nat of the natural numbers (or just Nat, if one is working in the Chapter2 namespace), setting up many of the basic results about these alternate natural numbers which parallel similar lemmas about {{\bf N}} that are already in Mathlib (but with many of these lemmas set as exercises to the reader, with the proofs currently replaced with “sorries”). Then, in an epilogue section, isomorphisms between these alternate natural numbers and the Mathlib natural numbers are established (or more precisely, set as exercises). From that point on, the Chapter 2 natural numbers are deprecated, and the Mathlib natural numbers are used instead. I intend to continue this general pattern throughout the book, so that as one advances into later chapters, one increasingly relies on Mathlib’s definitions and functions, rather than directly referring to any counterparts from earlier chapters. As such, this companion could also be used as an introduction to Lean and Mathlib as well as to real analysis (somewhat in the spirit of the “Natural number game“, which in fact has significant thematic overlap with Chapter 2 of my text).

The code in this repository compiles in Lean, but I have not tested whether all of the (numerous) “sorries” in the code can actually be filled (i.e., if all the exercises can actually be solved in Lean). I would be interested in having volunteers “playtest” the companion to see if this can actually be done (and if the helper lemmas or “API” provided in the Lean files are sufficient to fill in the sorries in a conceptually straightforward manner without having to rely on more esoteric Lean programming techniques). Any other feedback will of course also be welcome.

[UPDATE, May 31: moved the companion to a standalone repository.]



Source link

Analysis companion Lean
Share. Facebook Twitter Pinterest LinkedIn Tumblr Email WhatsApp Copy Link
yhhifa9
admin
  • Website

Related Posts

Math

A crowdsourced project to link up erdosproblems.com to the OEIS

September 2, 2025
Math

Mathletics Works: New Study Proves Clear Link to NAPLAN Success

August 31, 2025
Math

Math Conversion Chart | Metric Conversions

August 30, 2025
Math

Multiplication of Whole Numbers | Whole Numbers|Multiplication|Numbers

August 27, 2025
Math

Is math discovered or invented? – Math with Bad Drawings

August 26, 2025
Math

Learning Decision Process Theory with a Wolfram Language Toolkit—Wolfram Blog

August 25, 2025
Add A Comment
Leave A Reply Cancel Reply

Top Posts

2024 in math puzzles. – Math with Bad Drawings

July 22, 202520 Views

Testing Quantum Theory in Curved Spacetime

July 22, 20259 Views

How AI Is Helping Customer Support Teams Avoid Burnout

May 28, 20257 Views

Chemistry in the sunshine – in C&EN

August 9, 20256 Views
Don't Miss

Irina’s Spring Semester in Valencia, Spain 

By adminAugust 31, 20255

36 Eager to follow in the footsteps of a college student who studied abroad in…

Living Costs in Limerick | Study in Ireland

August 30, 2025

These 3 College Students Studied Abroad in Greece

August 27, 2025

Taylor’s Spring Semester in Athens

August 23, 2025
Stay In Touch
  • Facebook
  • Twitter
  • Pinterest
  • Instagram
  • YouTube
  • Vimeo

Subscribe to Updates

Please enable JavaScript in your browser to complete this form.
Loading
About Us
About Us

Welcome to Bkngpnarnaul. At Bkngpnarnaul, we are committed to shaping the future of technical education in Haryana. As a premier government institution, our mission is to empower students with the knowledge, skills, and practical experience needed to thrive in today’s competitive and ever-evolving technological landscape.

Our Picks

Making PD meaningful in today’s classrooms

September 2, 2025

Just 1 minute of vigorous exercise a day could add years to your life

September 2, 2025

Subscribe to Updates

Please enable JavaScript in your browser to complete this form.
Loading
Copyright© 2025 Bkngpnarnaul All Rights Reserved.
  • About Us
  • Contact Us
  • Disclaimer
  • Privacy Policy
  • Terms and Conditions

Type above and press Enter to search. Press Esc to cancel.