Skip to content

Instantly share code, notes, and snippets.

# -- HELM prompt, 8 shot, CoT? ref:,level=1,use_official_examples=False,use_chain_of_thought=True,model=01-ai_yi-34b/scenario_state.json,,level=1,use_official_examples=False,use_chain_of_thought=True,model=01-ai_yi-34b
"""Given a mathematics problem, determine the answer. Simplify your answer as much as possible.###
Problem: Let $r=3^s-s$ and $s=2^n+1$. What is the value of $r$ when $n=2$?
Answer: First substitute $n=2$ into the expression for $s$ to find $s=2^2+1=5$. Then substitute $s=5$ into the expression for $r$ to find $r=3^5-5=243-5=\\boxed{238}.###
Problem: If $x^{2y}= 4$ and $x = 4$, what is the value of $y$? Express your answer as a common fraction.
Answer: Plugging $x = 4$ into the first equation, we get $4^{2y} = 4^1 \\Rightarrow 2y = 1 \\Rightarrow y = \\boxed{\\frac{1}{2}}.###
Problem: If $y = \\dis
brando90 /
Created May 9, 2024 21:31
# -- Prompt minerva MATH 3 - better minerva + cot/scratch_pad
Find the domain of the expression $\frac{\sqrt{x-2}}{\sqrt{5-x}}$.}
Let's think step by step. The expressions inside each square root must be non-negative. Therefore, $x-2 \ge 0$, so $x\ge2$, and $5 - x \ge 0$, so $x \le 5$. Also, the denominator cannot be equal to zero, so $5-x>0$, which gives $x<5$. Therefore, the domain of the expression is $\boxed{[2,5)}$.
brando90 / gist:769e71f376b4a9a78ad63c6989be6a52
Last active May 9, 2024 05:11
import math
from pantograph.server import Server, ServerError
from pantograph.expr import GoalState, TacticHave, TacticCalc, Tactic
from loguru import logger
from dataclasses import dataclass, field
from typing import Optional, List, Tuple
class SearchResult:
"""The result of attempting to prove a theorem."""
brando90 /
Created April 25, 2024 17:45

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

references: -

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
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 / gist:0323f9e2a659580978ec5daa72f41333
Created March 2, 2024 23:50
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 / gist:0786c13414a510d4652351a2d96b51fc
Created March 2, 2024 20:52
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]
**Do not** run `` 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` 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]( does **not work**) with:
# -- Setup our lean_src_proj project for the first time (ref:
# - 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
# Byte-compiled / optimized / DLL files
# C extensions
# Distribution / packaging