# Exploring proofs for Sheldon Axler's *Linear Algebra Done Right*, Fourth Edition, 2024 > [! announcement] This is a UC Berkeley student project built to accompany Prof. Edward Frenkel's Math 110 Spring 2024 Abstract Algebra course. So far, we only do the obvious: explore the text, the lectures, the exercises and their solutions using Claude3 and GPT-4. We have expanded [[EF Solutions|Professor Frenkel's exercise solutions]] with examples across a variety of fields. This has led to: >- Vectorizing text using: >- LaTex representation (thank you, [Leslie Lamport](https://www.lamport.org/) ) >- LEAN representation: try [Play the Number Game](https://adam.math.hhu.de/#/g/hhu-adam/NNG4) to see where we are going. And here are [people working to put *LADR* in LEAN](https://leanprover.zulipchat.com/#narrow/search/axler) >- PDF extraction with Python tools >- hand-annotation for fine-grained LLM ingestion >**Next: develop new reading and writing tools using** >- Whisper transcription of lecture audio; lecture video image analysis, OCR >- Proof generation and testing: >- 3D representation of Frenkel's diagrams showing relationships among vector spaces, duals, and matrix representations > Do not rely on accuracy of proofs. All errors and mistakes are ours, the students building this open source project, and do not reflect on Professor Axler or Professor Frenkel. > - Inspiration: [Semantic Scholar](https://www.semanticscholar.org/product/semantic-reader) > > - Inspiration: [ProofNet](https://huggingface.co/datasets/hoskinson-center/proofnet) > > - use LEAN mathlib environment for interactive proof checking for LADR text, examples, exercises. See list of all LADR proofs now in Lean: [[Lean Proofs for Axler LADR Exercises]] > > - See [Lean in 2024](https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/) > > - Inspiration: [Xena Project](https://xenaproject.wordpress.com/what-is-the-xena-project/) ### Goal: build a formal environment to explore statements and proofs in **LADR** >[! Background machinery as of April 5, 2024] >Note: [new version of LADR 4e](https://linear.axler.net/LADR4e.pdf)was released on May 1, 2024; expect frequent updates by Professor Axler. > First phase of vectorization used copy/paste from PDF into embedding. Due to complicated structure of PDF, inaccurate formulations from original text were vectorized and embedded, creating some errors in proofs. Since Prof. Axler composed LADR originally in LaTeX, using the original would avoid the PDF to LaTeX step, and avoid this source of inaccurate representation. > **TO BE TESTED** > New corpus uses [Papermage](https://github.com/allenai/papermage) reconstruction of PDF for ingestion. Some parsing errors. >Vectorization and embedding of LADR and PDF's of Frenkel proofs done with tools from Anythings [MintPlex Anythings](https://github.com/Mintplex-Labs/anything-llm) linked to GPT-4 >March 4, 2024: new release of Claude may have surpassed GPT-4 in mathematics: we will redo LADR embedding and proofs using Claude, and compare quality of proofs #### Link LADR statements, proofs, examples, exercises - Challenge: generate proof-checked responses to problems, readings - [[Table of Exercises and Solutions]] --- > [!note]- Outline of Goals > - State problems, axioms, theorems in an interoperable format for [Retrieval Augmented Generation]() > - Inspiration: [ProofNet](https://huggingface.co/datasets/hoskinson-center/proofnet) > - link to mathematical systems: Mathematica, MAPLE, MACSYMA, >- use LEAN mathlib environment for interactive proof checking for LADR text, examples, exercises. See list of all LADR proofs now in Lean: [[Lean Proofs for Axler LADR Exercises]] >- Generate proofs using LLM, RAG systems >>- LLM: OpenAI, Google, Meta: see HuggingFaces > - Examine proofs >- expand proof checking groups to include larger student population and data science community >- use proof authenticators to validate LLM-generated proofs >- Coq; Isabelle; HOL Light; Lean; --- ![[V-T-V-Matrix.excalidraw.svg]] --- > [!info] Here's an example: February 29, 2024 Mock Midterm with answers generated by GPT-4 with Retrieval Augmented Generation of proofs > Mock Midterm answers from Professor Frenkel to come soon > Real Midterm questions and answers to come soon >  >[!info] **GPT-4 proposed answers to Mock Midterm: do not trust!** > [Mock Midterm GPT answers](Mock%20Midterm.md) > Note that GPT didn't get clean LaTeX for some questions, so gave strange answer. Under review. ### Materials from Math 110 - Readings: **LADR**; Hofstadter; Frenkel - Videos accompanying LADR: [Links to Axler text, videos](Links%20to%20Axler%20text,%20videos.md) <iframe src="https://linear.axler.net/LADRvideos4e.html" width="500" height="300"></iframe> - Formal Systems: [Hofstadter Notes on Formal Systems](https://cs.lmu.edu/~ray/notes/formalsystems/) html <iframe src=https://cs.lmu.edu/~ray/notes/formalsystems/ width="600"></iframe> - LADR, by chapters; with annotations and links ![[axler.pdf#height=200 width=700]]  ### Building a student's aide - Analyze LADR, by axiom,theorem, example, showing proofs or explanations: - develop visual sketch of ideas; - Link expanded text statements - to explanatory texts, further readings; - to other texts: Strang, - to LLM-generated discussions - Itemize Problems - By Chapter Section - By Frenkel assignments, chronologically - By Problem - Proofs - by Frenkel - by Axler - by GPT-4, LLAMA, - by GSI - by Lean - Lectures - Transcripts: embed in LLM - Notated lectures: ### Tools to explore - Github Copilot - Github Copilot generating code in Lean - VSCode - Lean Copilot - [Terence Tao](https://www.youtube.com/watch?v=AayZuuDDKP0) -  --- ### LEAN Proof Assistant [Lean](Lean.md) --- ![[TOC.excalidraw.svg]] --- ![[Welcome ChapXTheorem.excalidraw.svg]]