brando90

---- Prompts for Assessing & Rubber Ducking discussions on your research plan according to Vectoring ----

references: - https://web.stanford.edu/class/cs197/slides/04-vectoring.pdf

We should have three prompts. One tackling a different way to mitigate risks and uncertainties in projects with uncertainties -- especially in computer science and machine learning research. They are:

• Prompt 1: attempting to guess/extrapolate/identifying unknown unknowns -- to reduce risks we are unaware of.
• Prompt 2: asses my vectoring plan with assumptions for effective tackling of the unknown i.e., research

brando90

@inproceedings{langley00,
 author    = {P. Langley},
 title     = {Crafting Papers on Machine Learning},
 year      = {2000},
 pages     = {1207--1216},
 editor    = {Pat Langley},
 booktitle     = {Proceedings of the 17th International Conference
              on Machine Learning (ICML 2000)},
 address   = {Stanford, CA},
 publisher = {Morgan Kaufmann}

brando90

/-
theorem: lim_{x -> c+} f(x) = +infinity

x + infinit = +infinity

lim_{x -> c} f(x) = L
∀ ε > 0, ∃ δ > 0, 0 < |x - c| < δ → 0 < |f(x) - L| < ε

L = + infinity
consider some ε > 0

brando90

/-
-/
import Mathlib.Data.Real.Basic

-- define 1/x (reciprical) for reals
noncomputable def f (x : ℝ ):  ℝ := x⁻¹
#check f

-- unit test that f 1 = 1, f 2 = 1/2
theorem test_f1 : f 1 = 1 := by simp[f]

brando90

**Do not** run `install.sh` blindly. 
There is no guarantee it will work on your machine. 
Therefore, understand each command and only run the next command if the current one succeeded. 

## For developing Lean in this repo

If you git cloned this repo with say `git clone git@github.com:brando90/learning_lean.git` then you will have the lean project `lean_src_proj` folder and it won't have it's Lean depedencies e.g., Mathlib or the `.lake` folder will be missing. 

If that is the case, then you need to install mathlib for this project (note doing `lake +leanprover/lean4:nightly-2023-02-04 new my_project math` as suggested by the Lean [projects setup will fail](https://leanprover-community.github.io/install/project.html#creating-a-lean-project) does **not work**) with:
```bash

brando90

# -- Setup our lean_src_proj project for the first time (ref: https://leanprover-community.github.io/install/project.html#lean-projects)
# - Go to a folder where you want to create a project in a subfolder lean_src, and type lake +leanprover/lean4:nightly-2023-02-04 new lean_src math
# go to root of project (not the lean project)
cd $HOME/learning_lean
# Option1: set up the main lean_src_proj project for the first time:
# lake +leanprover/lean4:nightly-2023-02-04 new lean_src_proj math
# Option 2: set up main lean_src_proj project if you did a git clone of root learning_lean (so depedencies, e.g., matblib need to be installed)
# mkdir lean_src_proj
# cd lean_src_proj
# lake update

brando90

# Byte-compiled / optimized / DLL files
__pycache__/
*.py[cod]
*$py.class

# C extensions
*.so

# Distribution / packaging
.Python

brando90

Hi Lean Provers! Curious, I know that https://leanprover-community.github.io/mathlib4_docs/ is good for referencing the mathlib docs. If I want to see all of the main Lean4 syntax/constructs e.g., building types, strucs, functions, what is the recommended website? Similarly is there a cheat sheet/table for this?
1 reply


Jibiana Jakpor
  22 minutes ago
Functional Programming in Lean is a great resource for learning the syntax, especially for general purpose programming: https://leanprover.github.io/functional_programming_in_lean/. It doesn’t have much info on tactics though. That’s where MIL or Theorem Proving in Lean 4 will serve you bette


# Learning to write Lean

brando90

/-

-/
inductive UnaryNat : Type
| zero : UnaryNat
| succ : UnaryNat → UnaryNat
deriving Repr

#check UnaryNat
#check UnaryNat.zero

brando90

# -- make vscode workspace
# decided not to have name of repo cuz I'd need to have conda env + github repo match name for making things simpler
cd /afs/cs.stanford.edu/u/brando9/
vscode_file="vscode.gold-ai-olympiad.afs_snap.code-workspace"
echo $vscode_file
touch $vscode_file
echo '{
    "folders": [
        {
            "path": "gold-ai-olympiad"