Skip to content

Instantly share code, notes, and snippets.

View alreadydone's full-sized avatar

Junyan Xu alreadydone

197 followers · 795 following
View GitHub Profile
@alreadydone
alreadydone / 特吕弗论电影创作真诚与雄心.md
Created January 23, 2025 22:32
track down reference with DeepSeek-r1

Me:

Please find the original quote of the following Chinese translation:

我们千万不能跟自己说：由于想进入这个厉害的产业，所以必须在制片人的期望和自身的期望之间做出妥协，也就是一方面假装顺应他的要求而精心构思歌舞片或黑色电影，但另一方面又在里面放入一点自己的小想法，因为光是这样想，就已未战先败。我们应当跟自己说：我要给他们草草做一件绝对真诚的东西，以至于最终竟发出了真实的光芒，并展现出一股巨大的力量；我将要向他们证明，真实是可盈利的，而且我的真实是唯一的真实。[……]务必要疯狂地怀抱雄心，且还要疯狂地真诚……

DeepSeek: Retrieved 39 webpages

@alreadydone
alreadydone / Claude_trans_imports.md
Created November 27, 2024 02:30
Claude explaining #trans_imports PR https://github.com/leanprover-community/mathlib4/pull/19129/files

I'll break down this Lean code line by line:

elab tk:"#trans_imports" stx:(str)? : command => do
  • This line defines a custom Lean elaborator (command) named #trans_imports
  • tk:"#trans_imports" specifies the syntax for invoking this command
  • stx:(str)? means the command optionally takes a string argument
  • : command => indicates this is a command-level elaborator
  • do starts a do-block for sequential imperative-style operations
@alreadydone
alreadydone / claude-my-simp.md
Last active February 23, 2024 21:20
Claude-2.1's answer to a question about a custom `simp` tactic in Lean

Q: In Lean 4, how do I write a tactic that adds a fixed list of lemmas to a simp call?

A: Here is one way to write a tactic in Lean 4 that adds a fixed list of lemmas to a simp call:

import tactic

-- List of lemmas we want to add
def my_simp_lemmas : list name := [`foo, `bar, `baz]
@alreadydone
alreadydone / PolynomialReflection.lean
Last active February 11, 2024 04:13
Polynomial computations by reflection in Lean 4, using typeclass inference to build computable representations for expressions involving +,-,* etc.
import Mathlib.Data.Polynomial.Eval
open scoped Polynomial
open Polynomial (C X)
variable {R} [Semiring R] (p q : R[X])
class Polynomial.ComputableRepr where
coeff : ℕ → R
degreeBound : ℕ
@alreadydone
alreadydone / gist:5299197dc88b8237a4896803ac9a915f
Created November 22, 2023 03:05
Interesting `refine'` bug from CI run https://github.com/leanprover-community/mathlib4/actions/runs/6951956751/job/18914770581?pr=8556
2023-11-22T02:15:59.7794991Z error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/lean/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/CategoryTheory/Sites/Grothendieck.lean -R ././. -o ./.lake/build/lib/Mathlib/CategoryTheory/Sites/Grothendieck.olean -i ./.lake/build/lib/Mathlib/CategoryTheory/Sites/Grothendieck.ilean -c ./.lake/build/ir/Mathlib/CategoryTheory/Sites/Grothendieck.c
2023-11-22T02:15:59.7802783Z error: stdout:
2023-11-22T02:15:59.7805141Z ##[error]./././Mathlib/CategoryTheory/Sites/Grothendieck.lean:309:66: error: application type mismatch
2023-11-22T02:15:59.7806652Z completeLatticeOfInf
2023-11-22T02:15:59.7806982Z (WithTop
2023-11-22T02:15:59.8263195Z
@alreadydone
alreadydone / ProperlyDiscontinuous_CoveringMap.lean
Created October 6, 2023 09:01
A free and properly discontinuous action induces a covering map.
import Mathlib.Topology.Covering
import Mathlib.Topology.Instances.AddCircle
open Topology
variable {E X A : Type*} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A]
/- Note: WeaklyLocallyCompact + T2 actually implies LocallyCompact. -/
@[to_additive] lemma coveringMulAction_of_properlyDiscontinuousSMul {Γ T}
[TopologicalSpace T] [SMul Γ T] (cont : ∀ g : Γ, Continuous (fun t : T ↦ g • t))
@alreadydone
alreadydone / HomotopyLifting.lean
Last active October 23, 2023 05:48
The homotopy lifting property of covering maps.
/-
Copyright (c) 2023 Junyan Xu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Junyan Xu
-/
import Mathlib.Topology.Covering
import Mathlib.Topology.Homotopy.Path
import Mathlib.Topology.UnitInterval
/-!
@alreadydone
alreadydone / covariantClass_le_of_lt-trace.txt
Created August 24, 2023 14:27
timeout caused by `covariantClass_le_of_lt`
Before adding instance `covariantClass_le_of_lt`:
[Elab.command] [1.263200s] set_option profiler true in
@[simp]
theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
by
cases n
· simp [fin_one_eq_zero k]
rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
simp ▼
@alreadydone
alreadydone / np.show_config.txt
Last active July 21, 2023 16:36
HPC cluster node with Intel(R) Xeon(R) CPU E7-8860 v4 @ 2.20GHz or AMD EPYC 7543 32-Core Processor:
both the original (float64) and the float32 versions always yield 0.0
blas_info:
libraries = ['cblas', 'blas', 'cblas', 'blas']
library_dirs = ['/usr/local/Anaconda/envs/py3.9/lib']
include_dirs = ['/usr/local/Anaconda/envs/py3.9/include']
language = c
define_macros = [('HAVE_CBLAS', None)]
blas_opt_info:
define_macros = [('NO_ATLAS_INFO', 1), ('HAVE_CBLAS', None)]
@alreadydone
alreadydone / decomposition_monoid.lean
Last active July 7, 2023 07:42
Decomposition monoids, coprimality and square-freeness.
import Mathlib.Algebra.Squarefree
-- For definition of decomposition monoid and relative primeness, cf. https://link.springer.com/article/10.1007/s00233-019-10022-3
-- Discussion about the correct general definition of coprimality: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/IsCoprime.20is.20.40.5Bsimp.5D.3F
-- GCD monoids are decomposition monoids: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GCDMonoid/Basic.html#exists_dvd_and_dvd_of_dvd_mul
class DecompositionMonoid (R) [Semigroup R] : Prop where
exists_dvd_and_dvd_of_dvd_mul : ∀ m n k : R, k ∣ m * n → ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
theorem exists_dvd_and_dvd_of_dvd_mul' {R} [Semigroup R] [DecompositionMonoid R] {m n k : R}