| 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)) |
| /- | |
| 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 | |
| /-! |
| 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 ▼ |
| 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)] |
| 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} |
🎯 Solve the Riemann hypothesis.
Yoav Goldberg, April 2023.
With the release of the ChatGPT model and followup large language models (LLMs), there was a lot of discussion of the importance of "RLHF training", that is, "reinforcement learning from human feedback". I was puzzled for a while as to why RL (Reinforcement Learning) is better than learning from demonstrations (a.k.a supervised learning) for training language models. Shouldn't learning from demonstrations (or, in language model terminology "instruction fine tuning", learning to immitate human written answers) be sufficient? I came up with a theoretical argument that was somewhat convincing. But I came to realize there is an additional argumment which not only supports the case of RL training, but also requires it, in particular for models like ChatGPT. This additional argument is spelled out in (the first half of) a talk by John Schulman from OpenAI. This post pretty much
Make as much progress towards solving the Riemann hypothesis as you can.
April 18th, 2023
💀 Error
Progress
Name: SiegelGPT
Goal: Find out the status of Yitang Zhang's paper "Discrete mean estimates and the Landau-Siegel zero".
Embarking on a new goal:Find out the status of Yitang Zhang's paper "Discrete mean estimates and the Landau-Siegel zero".
Thinking...
Added task:Search for Yitang Zhang's paper "Discrete mean estimates and the Landau-Siegel zero"
Added task:Find out if the paper has been published in a journal or conference proceedings
Added task:Check for any news or updates on the status of the paper
Thinking...