Update all active specs, scripts, and architecture docs to reflect that
the original TestBed VPS (67.205.155.108) died on 2026-04-04 and Bezalel
has been migrated to share the Allegro VPS (167.99.126.228).
Files updated:
- specs/wizard-vps-houses-deployment.md: mark TestBed as DEPRECATED,
update Bezalel IP to 167.99.126.228 with migration note
- specs/wizard-telegram-bot-cutover.md: update Bezalel host references,
SSH command, and add deprecation note
- uni-wizard/v4/FINAL_ARCHITECTURE.md: update bezalel endpoint
- scripts/wire_wizard_telegram_bots.sh: update SSH target for Bezalel
The old IP is retained only in explanatory comments noting the migration.
Closes#506
2026-04-22 02:40:20 -04:00
5 changed files with 15 additions and 179 deletions
| **Small lemma** | Missing but straightforward piece in an active area (e.g., "Proposition 3.2 in Smith 2021 needs this case analysis") | Check paper + 1–2 related references; prove or give counterexample | Clarifies existing theory, removes ambiguity |
| **Counterexample search** | Find explicit counterexample to a claimed-but-unproven statement (often from MO/SE) | Compute/construct + cite the original claim | Prevents propagation of errors |
| **Computational classification** | Exhaustive enumeration/classification of a small infinite family (e.g., "all groups of order < 200 with property X") | Code is verifiable; results match known data | Creates reference data, spotlights patterns |
| **Formalization gap** | Statement already believed true but missing from Lean/mathlib/Isabelle | Formal proof artifact; merges to mainline library | Makes mathematics machine-checkable |
| **OEIS sequence note** | New sequence entry or correction to an existing entry with proof/algorithm | OEIS A-number + formula/generation code | Public archival, enables further work |
| **Exposition repair** | Fix an unclear proof, fill a gap, simplify an argument in an existing paper | Side-by-side diff + justification for each change | Improves pedagogy, reduces confusion |
| **MathOverflow-quality answer** | Answer to a specific, bounded, research-level question on MO/SE that has no accepted answer | Cite question + self-contained proof/computation | Serves the community directly |
---
## Rejection Criteria (No-Crank Guardrails)
> Any candidate that triggers one or more of these is **rejected outright** — no scoring needed.
| Rule | What to look for | Why it's crank |
|------|------------------|----------------|
| **Unsourced grand theory** | Claim introduces new "framework"/"paradigm" without citing specific bounded problem it solves | Mathematics advances by solving problems, not proposing frameworks |
| **Impossible scope** | "I will prove/disprove the Riemann Hypothesis", "classify all finite simple groups" | Demonstrably beyond single-attack capability |
| **No verification path** | No way for a third party to check the work (no code, no formalization, no explicit examples) | Cannot be wrong if it cannot be checked |
| **Novelty claim without literature search** | States "I believe this is new" without checking MathSciNet/arXiv/Google Scholar | Almost certainly reinvention or known result |
| **Vague mathematical objects** | Uses undefined or ambiguous terminology ("energy", "resonance", "harmonic" in non-standard ways) | Not mathematics |
| **Secrecy or paywall** | Key definition or proof behind a paywall or withheld | Not sovereign; not verifiable |
| **Symbolic overloading without definition** | Repurposes standard notation in non-standard ways without explicit redefinition | Creates confusion, not clarity |
| **Invariance violations** | Claims "up to isomorphism" or "modulo equivalence" without defining the equivalence relation | Not mathematically precise |
| **Cherry-picked examples as proof** | Proves only easy special cases and claims the general case follows | Example ≠ theorem |
| **Circular citation chains** | Relies on unpublished/preprint work that itself cites the candidate as motivation | Not a foundation |
| **No clear problem statement** | Cannot write a one-sentence problem statement in standard mathematical English | Not a problem; just musings |
| **Claims of "obvious" or "clear" for non-trivial steps** | Uses "obviously" or "it is clear that" where a proof requires >2 lines | Evasion |
| **References only popular science / non-technical sources** | Cites Penrose, Hawking, Tegmark for technical claims | Wrong tier of source |
| **All notation defined in non-standard way** | Redefines basic operators (+, ×, ≤) without explicit warning | Not mathematics |
| **No engagement with existing literature** | Zero citations to relevant peer-reviewed work or established preprints | scholarship was not done |
| **Claims of "disproof" of widely-accepted theorems** | Without finding a peer-reviewed error in the existing proof | Almost certainly wrong |
---
## Evidence Tiers
| Tier | Artifact | What it Proves |
|------|----------|----------------|
| **T3 — Literature** | MathSciNet / Zentralblatt / Google Scholar citations showing the problem is real and open | Problem exists in the literature |
| **T2 — Executable** | Python/Sage/Lean code that others can run to verify computation/formalization | Result is reproducible |
| **T1 — Human-reviewed** | MO answer with upvotes, referee report, or explicit external review | Independent verification |
| **T0 — Self-contained** | Clear statement + proof/computation in a single document, all definitions explicit | Standalone correctness |
A valid candidate must have at least **one** T3 citation (shows the problem is real) AND a verification artifact (T0 minimum; T2 ideal).
---
## Scoring Rubric
Score each candidate on **4 dimensions**, each 0–3. Maximum 12 points.
| **Boundedness** | Scope is explicitly finite/small (single lemma, finite classification < N, one SE question) | Scope is implied bounded but not quantified | Scope is large/vague but attackable | Unbounded or impossible scope |
| **Verifiability** | T2 artifact (code/formalization) + T3 citation | T0 proof + T3 citation | Proof/computation only, no citations | No way to check independently |
| **Usefulness** | Solves problem others actively need (cites known difficulty, fills formalization gap) | Solves a clean exercise or interesting special case | Interesting but no clear audience | Pointless or self-referential |
| **Discipline** | No crank flags; explicit rejection criteria cleanly passed | Minor crank flags (vague wording) but overall sound | Some crank flags but bounded scope rescues it | Triggers multiple rejection rules |
**Thresholds**:
- **8–12**: Legitimate shadow maths candidate — queue for work
**Candidate**: "Proposition 3.2 in 'Coarse Geometry and Coarse Embeddings' (Lang-Schlichenmaier 2005) states that every finite CW-complex has Markov property. The proof gives 'it follows by induction on skeleta' without handling the attaching map case. Fill the gap."
**Triage**:
- **Category**: Small lemma (exposition repair + proof gap fill)
- **Boundedness**: 3 — single proposition in a specific paper, 2–3 pages max
- **Verifiability**: 3 — paper is cited (T3), self-contained proof in 20 lines (T0), can formalize in Lean (T2 possible)
- **Usefulness**: 3 — readers of this paper hit this gap; Lean formalization needed for mathlib
- **Discipline**: 3 — no crank flags; scoped, sourced, technical
- **Total**: **12/12** → YES
**Action**: File ticket "MATH-LEMMA-001"; assign to formalization lane + human review.
---
### Example 2: Grand Unified Theory — CRANK
**Candidate**: "I have discovered the Energy-Conscious Riemann Hypothesis framework. The zeros of ζ(s) correspond to harmonic resonance frequencies in prime-number energy manifolds. Uses my new Operator-Weight theory."
**Triage**:
- **Category**: N/A
- **Rejection triggers**:
- ✗ Unsourced grand theory (introduces "Energy-Conscious", "Operator-Weight" with no definition in standard math)
- ✗ No verification path (no computation, no reference to known data)
**Action**: Close with reason "crank: unsourced grand theory + no verification path".
---
### Example 3: Computational Classification — Bounded
**Candidate**: "Compute all 3-headed Turing machines with 3 states that halt within 100 steps on the blank tape. There are 9 such machines. This fills an OEIS gap: A327000 only lists up to 2-state 2-symbol."
@@ -10,9 +10,12 @@ This document records the first concrete house layout for Ezra and Bezalel.
- Role: repo / Gitea / architecture wizard house
### Bezalel host
- VPS: TestBed
- Public IP: `67.205.155.108`
- VPS: TestBed (DEPRECATED — original VPS at 67.205.155.108 unreachable since 2026-04-04)
- Public IP: `167.99.126.228` (shared with Allegro VPS)
- Role: forge / test / optimization wizard house
- Migration: Bezalel services colocated with Allegro after TestBed VPS failure
> Note: The original TestBed VPS (67.205.155.108) is dead. Bezalel was migrated to share the Allegro VPS (167.99.126.228) to restore CI testbed and wizard house functionality. See #506.
endpoint:http://167.99.126.228:8643 # Shared with Allegro after TestBed VPS death (was 67.205.155.108)
role:artificer
```
Reference in New Issue
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.