Lean files for class

Stream: Lean for Scientists and Engineers 2024

[Tyler Josephson ⚛️]

Find the Lean files for class here!

[Tyler Josephson ⚛️]

Lecture1.lean

[Tyler Josephson ⚛️]

Lecture2.lean

[Tyler Josephson ⚛️]

Lecture2_post_lecture.lean

[Tyler Josephson ⚛️]

Lecture3.lean

[Tyler Josephson ⚛️]

Lecture4.lean

[Tyler Josephson ⚛️]

Lecture4_post_lecture.lean

[Tyler Josephson ⚛️]

Lecture5.lean

[Tyler Josephson ⚛️]

Lecture6.lean

[Tyler Josephson ⚛️]

Lecture6_post_lecture.lean

[Tyler Josephson ⚛️]

Lecture7.lean

[Tyler Josephson ⚛️]

Lecture8.lean

[Tyler Josephson ⚛️]

Lecture8_post_lecture.lean

[Tyler Josephson ⚛️]

Lecture-9-lists-arrays-indexing-IO.zip

[Tyler Josephson ⚛️]

Lecture9.lean

[Notification Bot]

A message was moved here from #Lean for Scientists and Engineers 2024 > Lecture recordings by Tyler Josephson ⚛️.

[Tyler Josephson ⚛️]

Files for class will be in these GitHub repos:
LeanBET and LeanMD

[Eric Taucher]

(deleted)

[Tomas Skrivan]

I have set up a github repository for Wednesday lecture so you can follow the lecture on your computer. In the lecture, I will go over the Main.lean file which demonstrates the main capabilities of SciLean right now.

I have also started writing reference manual for SciLean. Right now, it contains only the first chapter on (n-dimensional) arrays and it is still very rough but it might be of interest.

[Bulhwi Cha]

I found a small typo in README.md: https://github.com/lecopivo/SciLeanDemo/pull/1.

[Eric Taucher]

For those not familiar with approximating Ordinary differential equations (ODE) using Runge-Kutta 4 (RK4) it might be worth taking a few minutes to learn about it.

Until I actually needed to know how to solve ODEs as a programmer I always assumed that ODEs would be solved symbolically then learned of RK4 and was glad to have learned it.

[Kevin Buzzard]

Most ODEs cannot be solved symbolically! (if I've understood correctly what "symbolically" means)

[Eric Taucher]

Kevin Buzzard said:

(if I've understood correctly what "symbolically" means)

Yes you did.

I am not a mathematician but a humble programmer. I did sign up then drop a class in differential equations thinking I would never use it again in programming. That was 40 years ago. However I did take a class in numerical methods and that was quite useful but I don't remember getting to RK4. After many years I needed to learn how to do ODEs for biological simulations and a book noted the use of RK4. It was one of those times in life where I had to mentally erase that fallacy to take a step in the right direction.

On a side note, do you know of a blog entry or page that explains why "most ODEs cannot be solved symbolically!" You might be surprised at how popular such a link would be for programmers trying to solve ODEs who still think that they should be solved symbolically. :smile:

Thanks.

[Kevin Buzzard]

Most integrals cannot be solved symbolically so I guess it follows from that

[Eric Taucher]

Hopefully this reply is not to far from the topic of being useful to other scientists and engineers following this class.

Using ChatGPT 4o

Prompt:

Some math problems can not be solved symbolically such as ordinary differential equations. What are other examples of math problems that can not be solved symbolically starting from a symbolic expression?

Completion:

There are several types of mathematical problems that cannot be solved symbolically, meaning they don't have closed-form solutions or exact symbolic representations. Here are some examples:

1. Nonlinear Equations

- Many nonlinear equations, especially higher-degree polynomials beyond the fourth degree, cannot be solved symbolically. For example, the general quintic equation (fifth-degree polynomial) cannot be solved using radicals, as established by the Abel-Ruffini theorem.

2. Partial Differential Equations (PDEs)

- Many PDEs, such as the Navier-Stokes equations in fluid dynamics, do not have known symbolic solutions in the general case. Solutions often require numerical methods or approximations.

3. Transcendental Equations

- Equations involving transcendental functions (like exponential, logarithmic, trigonometric, etc.) often do not have closed-form solutions. An example is \( x = e^{-x} \), which cannot be solved exactly for \( x \) in terms of elementary functions.

4. Optimization Problems

- Many optimization problems, especially those involving nonlinear objective functions or constraints, do not have closed-form solutions. Problems such as finding the global minimum of a non-convex function often require numerical methods.

5. Integration Problems

- Some integrals cannot be expressed in terms of elementary functions. A classic example is the integral \( \int e^{x^2} dx \), which does not have a symbolic solution and is usually expressed in terms of the error function \( \text{erf}(x) \).

6. Special Functions

- Solutions involving special functions (like the gamma function, Bessel functions, or elliptic integrals) are often not solvable symbolically except in very specific cases. These functions themselves are often defined by integrals or series that cannot be simplified further symbolically.

7. Discrete Dynamical Systems

- Some discrete dynamical systems, such as those governed by certain recurrence relations, do not have closed-form solutions. For instance, the general solution to nonlinear recurrence relations often cannot be expressed symbolically.

8. Diophantine Equations

- Many Diophantine equations, which seek integer solutions to polynomial equations, do not have general symbolic solutions. For example, there is no general method to solve the equation \( x^n + y^n = z^n \) (for \( n > 2 \)) in integers, which is related to Fermat's Last Theorem.

9. Systems of Equations

- Some systems of equations, particularly nonlinear or higher-dimensional systems, cannot be solved symbolically. This is common in systems arising in areas such as game theory or economic modeling.

10. Fractals and Chaotic Systems

- Equations describing fractals or chaotic systems often do not have symbolic solutions, as their behavior is inherently complex and sensitive to initial conditions.

These examples illustrate the wide range of mathematical problems where symbolic solutions are either impossible or impractical, necessitating the use of numerical methods, approximations, or special functions.

[Tyler Josephson ⚛️]

Kevin Buzzard said:

Most integrals cannot be solved symbolically so I guess it follows from that

This is how I think about it, too.

[Tomas Skrivan]

I updated today lecture repository with a file containing widget visualizing wave equation simulation. If you open it up and place cursor on the last line

#html <SvgWidget html={init.html} state={init.state}/>

you should see
Peek-2024-08-21-10-22.gif

I would appreciate if someone tries it as I was having a trouble running it on my home computer yesterday evening.

[Eric Taucher]

FYI

I tried it on Windows 11 and it failed. Currently chatting with Tomas in private.

What I did was go to the GitHub repository and follow the instructions: https://github.com/lecopivo/SciLeanDemo/tree/master

Seems some of you did get it to work so curious as to how you did it if using Windows 11.

[Martin Dvořák]

I got an error:

Some required builds logged failures:
- Batteries.CodeAction.Attr:dynlib
error: build failed

[Eric Taucher]

Martin Dvořák said:

I got an error:

Some required builds logged failures:
- Batteries.CodeAction.Attr:dynlib
error: build failed

Yes.

As suggested by Tomas, I also tried another Mathlib4 project. As I did not have one on my machine I used just https://github.com/leanprover-community/mathlib4 from the VSCode Lean 4 extension and it resulted in an error at import Batteries in Mathlib.lean.

Tomas also suggested I open an error report but know someone with more Lean experience than me should easily find it and give a better report to more quickly get it resolved.

[Martin Dvořák]

I have Windows 10 and after opening Main.lean in VS Code, I get the following error in the Infoview:

`c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\lake.exe setup-file C:/Users/mdvorak/Documents/SciLeanDemo/Main.lean Init SciLean` failed:

stderr:
⚠ [1798/2604] Replayed SciLean.Analysis.AdjointSpace.AdjointProj
warning: .\.\.lake/packages\scilean\.\.\SciLean\Analysis\AdjointSpace\AdjointProj.lean:573:0: using 'exit' to interrupt Lean
✖ [1881/2604] Building Batteries.CodeAction.Attr:dynlib
trace: .> c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\leanc.exe -shared -o .\.\.lake/packages\batteries\.lake\build\lib\Batteries-CodeAction-Attr-1.dll .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Attr.c.o.export -L.\.\.lake/packages\batteries\.lake\build\lib
info: stderr:
ld.lld: error: undefined symbol: lean_decl_get_sorry_dep
>>> referenced by .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Attr.c.o.export:(l_Std_CodeAction_initFn____x40_Batteries_CodeAction_Attr___hyg_792____lambda__4)
>>> referenced by .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Attr.c.o.export:(l_Std_CodeAction_initFn____x40_Batteries_CodeAction_Attr___hyg_792____lambda__4)
>>> referenced by .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Attr.c.o.export:(l_Std_CodeAction_initFn____x40_Batteries_CodeAction_Attr___hyg_792____lambda__4)
>>> referenced 3 more times
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\leanc.exe' exited with code 1
⚠ [2527/2604] Replayed SciLean.Lean.Meta.Replace
warning: .\.\.lake/packages\scilean\.\.\SciLean\Lean\Meta\Replace.lean:166:0: using 'exit' to interrupt Lean
⚠ [2528/2604] Replayed SciLean.Lean.Meta.LiftLets
warning: .\.\.lake/packages\scilean\.\.\SciLean\Lean\Meta\LiftLets.lean:169:0: using 'exit' to interrupt Lean
⚠ [2583/2604] Replayed SciLean.Tactic.AnalyzeLambda
warning: .\.\.lake/packages\scilean\.\.\SciLean\Tactic\AnalyzeLambda.lean:209:0: using 'exit' to interrupt Lean
Some required builds logged failures:
- Batteries.CodeAction.Attr:dynlib
error: build failed

[Eric Taucher]

Martin Dvořák said:

I have Windows 10 and after opening Main.lean in VS Code, I get the following error in the Infoview:

I used WIndows 11 and get the exact same, so it is reproducible.

[Tomas Skrivan]

Looks like Batteries issue as it breaks on

✖ [1881/2604] Building Batteries.CodeAction.Attr:dynlib
trace: .> c:\Users\mdvorak\.elan\toolchains\leanprover--lean4---v4.11.0-rc2\bin\leanc.exe -shared -o .\.\.lake/packages\batteries\.lake\build\lib\Batteries-CodeAction-Attr-1.dll .\.\.lake/packages\batteries\.lake\build\ir\Batteries\CodeAction\Attr.c.o.export -L.\.\.lake/packages\batteries\.lake\build\lib
info: stderr:
ld.lld: error: undefined symbol: lean_decl_get_sorry_dep

everything else is warnings. Not sure what to do about this :(

Is for example ProofWidgets building for you?

[Asei Inoue]

(deleted)

[Asei Inoue]

(deleted)