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

University of Virginia President Resigns After Trump’s Demands

June 28, 2025

X-ray boosting fabric could make mammograms less painful

June 28, 2025

Wolfram Education Programs for Middle School, High School and Beyond—Wolfram Blog

June 28, 2025
Facebook X (Twitter) Instagram
Sunday, June 29
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

Wolfram Education Programs for Middle School, High School and Beyond—Wolfram Blog

June 28, 2025
Math

Case Study: How International School Utrecht Found Success with Mathletics and Mathseeds

June 27, 2025
Math

Introducing Wolfram Notebook Assistant—Stephen Wolfram Writings

June 26, 2025
Math

What is Bills in Maths? |Use of Bill

June 25, 2025
Math

A survey of recent works in Oulipo. – Math with Bad Drawings

June 24, 2025
Math

Orders of infinity | What’s new

June 23, 2025
Add A Comment
Leave A Reply Cancel Reply

Top Posts

10 Student Engagement Strategies That Empower Learners –

May 28, 20253 Views

Do You Hear What I Hear? Audio Illusions and Misinformation

May 28, 20253 Views

Improve your speech with immersive lessons!

May 28, 20252 Views

Arabic poetry, with a special focus on Palestine – Global Studies Blog

May 28, 20252 Views
Don't Miss

Open Access Week 2023–South Asia Resources

By adminJune 28, 20250

Open Access Week 2023 To suggest new content for SAOA, use the suggestion form. Source…

Best Abroad Study Consultants Near Me

June 27, 2025

Hayley’s Spring Semester in Maynooth

June 26, 2025

Study MD MS in UK Without PLAB

June 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

University of Virginia President Resigns After Trump’s Demands

June 28, 2025

X-ray boosting fabric could make mammograms less painful

June 28, 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.