patonotes

[patonotes]

Prompt for notebook LLM

One of you, a host, is an expert with a PhD in mathematics. The other one of you, another host, has a PhD in machine learning. You are both knowledgeable in LEAN and theorem proving. You have written articles and blogs on them. You always talk about a topic based on information from the sources only. Your reputation as precise and reliable experts is super important for you. Your podcast and conversation is a class at an Ivy League university attended by experts in machine learning and mathematics. Your audience consists of PhD students in mathematics and machine learning. If you are more than 40% unsure about something, don't guess. You will say that you don't know. If you are guessing or interpreting between 5% and 20% of an answer. You will always say that percentage. Your answers align with the sources without interpretation.

[patonotes]

Teaching AG

I will teach the first course in AG. My strategy this time around will be:

Introducing affine varieties (3 weeks). Their topology (week 1), their functions (i.e., structure sheaf) (week 2), and their morphisms (week 3).

Introducing projective varieties. The topology (week 1), their functions (week 2), and their morphisms (week 3).

Introducing Sheaf theory. Their definition (week 1). Examples (week 2), and their morphisms (week 3).

[patonotes]

More poems

Poema to Atenas

A veces veo a Atenas. Tranquila, serena. En que pensara, una vez ha comido? En el cero? El infinito? El caos, lo indecidible? En los numeros que no se llegan ni contando En el sexo? Acaso en el tiempo. En el programa, que a hurtadillas furtiva observa desde la cocina. En la cabala, las mil combinaciones En el nombre secreto de Dios, del ella, el mio. Da lo mismo. Acaso su alma reposa de alivio,

la veo…se me acerca. Su boca detiene un barco de juguete Sus ojos tiene paz, los mios angustia, Conoce acaso la pregunta que prefijo a Bruno a la hoguera, y en la noche agazapada me atormenta.

Bosteza, se echa. En sus ojos se halla la premisa que un angel en el paraiso susurro a Eva: Tranquila, disfruta, que el vivir es lo unico que al fin cuenta queda.

[patonotes]

Poems to Oggy

Title: Pato and Oggy

A tale of love and treats, Eyes locked with eager gaze, Is it me or snacks?

Title: "Oggy, El Grumpy"

En la calle, walking with my dog, Oggy, Cartera vacía, but to me, he's worth a bounty. His surgery costly, aún así, él está grumpy.

Oggy, Oggy, con su cara de grumpy, After all, él es mi amigo, my loyal puppy. Aunque se enoje, it's part of our journey, Oggy, el grumpy, but I adore him, trust me.

Branka's patience, in her eyes, amor puro. Oggy bit her once, yet their bond was now secure. El cariño es real, Grumpy or not, Oggy's love, siempre profundo.

[patonotes]

Using several LLMs

We have the insight that using LLM that are fined tuned for a particular task may improve the performance: The candidates as on May 2025 ar:

For writing statements and problems: Herarld https://openreview.net/pdf?id=Se6MgCtRhz#page=13.85

To improve and correct a proof: Improver https://arxiv.org/pdf/2410.04753

To prove DeepProver

Also some techniques like checking the type consistency: https://arxiv.org/pdf/2406.07222

[patonotes]

Using my LLM in Google cloude

After starting the VM and connecting to its on the terminal via

gcloud compute ssh ...

Now, I connec my VS into my VM. Next, I start the virtual environment for the LLM:

source herald_env/bin/activate

To create a file in the terminal, I used

touch file_name.txt

Now, I edit that file in the VS on my computer

[patonotes]

Moving files among Lean folders

Just moving the files does not run. I try lake update. lake exe cache get lake build (it is taking a long time)

I re-start the lean server in the VS code, and then re-start files. It takes 30min and still not working. Next, I quit VS and I start again.

I also run lake exe cache get inside the files where the files exist.

It runs!

[patonotes]

Updating the GitHub

My goal is that the folders in the Mac are synchronized with the Github, so I can work on either the mac or the VM.

The folder abelian_covers is up to date. I also clone the lean-app where we are writing the user cases. I will not update the Career grant. I have a big lean folder, inside I have lean-4-app (updated), but I also have LinearAlgebraProofs (probably erase), mathematics_in_lean, mechanics_of_proofs, project_V1 (probably to earase, and quivers(probably to erase).

Basically, I want to have a single linear algebra lean folder - the one of the lean4-app. I am not going to work on the Quivers now, so I should erase it. Project v1 has things that were trial-error.

I also have a folder called leanCopilot, macaula2 (for the user cases) and various.

[patonotes]

Testing Lean incomplete proofs

I have been thinking about unit test for LEAN4. It is still unclear to me how to write them. However, I discovered that we can use a combination of "#guard_msgs in" and "diagnosis" and "#print" to compile files with wrong proofs. I can detect the wrong proof because it includes a "sorry" in the output message.

The following is the first instance that I discovered that:

import Mathlib.LinearAlgebra.Basis.Basic

-- field we are working on

variable {F : Type*} [Field F]

-- define vector space V

variable {V : Type*} [AddCommGroup V] [Module F V]

-- define vector space W

variable {W : Type*} [AddCommGroup W] [Module F W]

-- label used to define basis on V and W

variable {k : Type*}

--define a basis in V and W

variable (v: Basis k F V)

variable (w: k → W)

-- construct a linear map given the value at the basis

noncomputable def R : V →ₗ[F] W :=

Basis.constr v F w

/--

error: unknown identifier 'i'

---

error: unsolved goals

case h.right

F : Type u_1

inst✝⁴ : Field F

V : Type u_2

inst✝³ : AddCommGroup V

inst✝² : Module F V

W : Type u_3

inst✝¹ : AddCommGroup W

inst✝ : Module F W

k : Type u_4

v : Basis k F V

w : k → W

f : V →ₗ[F] W

hf : ∀ (i : k), f (v i) = w i

⊢ ∀ (i : k), f (v i) = w i

-/

#guard_msgs in

lemma unique_linear_map_of_basis_v2 : ∃! (R : V →ₗ[F] W), ∀ i, R (v i) = w i := by

use Basis.constr v F w

constructor

· intro i

simp [Basis.constr_apply]

· intros f hf

apply Basis.ext v

--intro i

simp [hf i] -- missing hf

set_option diagnostics true

#print unique_linear_map_of_basis_v2

[patonotes]

Running files in the terminal

I want the file to be in lean project. So it must have

lakefile.lean lean-toolchain my_code.lean

the lakefile of lean should have

require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

i should be able to run

lake update -- This is not necessary! lake exe cache get -- This is important for every file! lake build

now, it runs lake env lean Test.lean

Remark. After night: I was wrong. It runs because my current Test.lean does not ask for Mathlib. The file does not run when I use that import. I run lake update, but this takes a long time. It does not work. Now, I try "lake exe cache get" This seems to work. Although, it does not return any feedback.

[patonotes]

Creating projects in LEAN4

The following work in April 23, 2025. I entered the code in terminal of my Mac

lake +leanprover/lean4:nightly-2024-04-24 new my_project math

this creates the folder my_project/

it ask me to restart the server and file. In the infoview it says server ready to start. Now, I go inside the folder my_project and I type

lake update.

The lake update went well, and it runs. However, the infoview still says "Waiting for the server to start." In the output, I have the error:

"Client is not running and can't be stopped. Its current state is: starting" I killed the terminal.

The computer seems in a loop. However, here, I just need to restart the VS code. Now, it is working!

[patonotes]

 “when I wrote it only God and I knew—now, God alone knows!”

[patonotes]

Amazing discussion about quantum computing

[patonotes]

Illustration math

The is work by Martin in Seatle University of Washington that makes a very nice case for illustrations

http://mkweb.bcgsc.ca/pi/piday2015/methods.mhtml

In particular, he has the illustration of the pi numbers as constellations of the sky

[patonotes]

This artist uses equations the way that I was planning to do it.  The idea that I will pursue is to make an exhibition called “integrals” and to play with the concept of incrementally hard and the J.L. Borges idea of the “The Garden of Forking Paths”

[patonotes]

the original is here 

http://www.smbc-comics.com/comic/2013-06-16