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

K-12 Gamification: A Guide For Publishers

September 23, 2025

Can Plantar Fasciitis Cause Knee Pain? Know the Link

September 23, 2025

The Purpose of a Classroom Observation for Gathering Data

September 23, 2025
Facebook X (Twitter) Instagram
Tuesday, September 23
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 Read4 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

Operations On Whole Numbers | Properties

September 22, 2025
Math

Representation of Whole Numbers on Number Line

September 19, 2025
Math

Smooth numbers and max-entropy | What’s new

September 18, 2025
Math

The Ruliology of Lambdas—Stephen Wolfram Writings

September 16, 2025
Math

12 Times Table | Read and Write Multiplication Table of 12 Video Trick

September 13, 2025
Math

Worksheet on Subtraction of Whole Numbers

September 10, 2025
Add A Comment
Leave A Reply Cancel Reply

Top Posts

2024 in math puzzles. – Math with Bad Drawings

July 22, 202521 Views

Testing Quantum Theory in Curved Spacetime

July 22, 202514 Views

How AI Is Helping Customer Support Teams Avoid Burnout

May 28, 202510 Views

Chemistry in the sunshine – in C&EN

August 9, 20258 Views
Don't Miss

Can I Use Financial Aid for a Study Abroad Program?

By adminSeptember 23, 20251

248 Are you wondering how to pay for study abroad? You’re not alone! Cost concerns…

What I Wish I Knew Before Starting University | Study in Ireland

September 22, 2025

Meet Four College Students Who Studied Abroad in England

September 19, 2025

Literary Gardens – Global Studies Blog

September 16, 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

K-12 Gamification: A Guide For Publishers

September 23, 2025

Can Plantar Fasciitis Cause Knee Pain? Know the Link

September 23, 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.