Junyan Xu alreadydone

Summary of changes for run 36d89d5f-d143-4477-adbe-d79566d5ad99

I filled all the sorrys in Aristotle28/StrongRankCondition.lean. Here's what was done:

Key Discovery: `adjp_none_some` was incorrectly stated

The original statement A.adjp s none (some i) = (A.submatrix some (Function.update some i none)).detp s was false — I verified this computationally with a 3×3 matrix where the LHS was 24 but the RHS was 36. The correct formula is:

A.adjp s none (some i) = (A.submatrix (Function.update some i none) some).detp (-s)

Question:

There are many here who both believe that soon AI will be superhuman at maths, solving all Millenium problems and beyond, and yet also reject any claims that maths is 'dead', and believe that mathematics will thrive.

I'm curious, for those people, what is maths in that future?

Answer:

First of all, let me state that I'm not sure that I am one of those people who believe that mathematics will thrive in the near or far future, but this has been on my mind for some time and I figured I would get out my own thoughts on the issue.

Q: What is causing CI to hang after completing the "lint mathlib" step when run on branches of forks of @leanprover-community/mathlib4 ? Answer after browsing the repository thoroughly.

A: Upon reviewing the repository and its scripts, certain patterns and possible causes of CI hanging after the "lint mathlib" step when run on forks can be identified:

Probable Cause:

Fork and Remote Configuration:
- Functions like gh_get_all_forks, gh_find_mathlib_fork, and gh_get_mathlib_fork in scripts/githelper.py involve verifying remotes for forks. If these functions encounter errors or inconsistencies in how the forks are set up or synchronized, it might lead to issues in downstream processes during the CI pipeline.
Error Handling in Fork Migration:

Me:

Please find the original quote of the following Chinese translation:

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

DeepSeek: Retrieved 39 webpages

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

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]

	import Mathlib

	variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
	variable [Module.Invertible R M]

	/-!
	# Invertible modules are Zariski-locally free

	We show that an invertible module over a commutative semiring is Zariski-locally free of rank 1,
	and that over a local semiring it is free.

	import Mathlib.Algebra.Algebra.Basic
	import Mathlib.Algebra.Polynomial.Basic
	import Mathlib.Algebra.Polynomial.Degree.Definitions
	import Mathlib.Algebra.Polynomial.Degree.Operations
	import Mathlib.Algebra.Polynomial.Eval.Coeff
	import Mathlib.Data.ZMod.Defs
	import Mathlib.Tactic.SuppressCompilation

	open scoped Polynomial
	open Polynomial (C X)


	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