segment-tree
/ ALaCarte-safe.lean
Last active
February 13, 2026 16:36
Data Types à la Carte for lean4
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- ========================================== | |
| -- 1. 基础架构：W-类型 (MLTT 核心) | |
| -- ========================================== | |
| inductive W (A : Type) (B : A → Type) where | |
| | mk (a : A) (f : B a → W A B) : W A B | |
| def wInd {A : Type} {B : A → Type} {p : W A B → Type} | |
| (step : (a : A) → (f : B a → W A B) → (∀ (b : B a), p (f b)) → p (W.mk a f)) | |
| (t : W A B) : p t := |
qunash
/ grpo_qwen-0-5b_single_t4.ipynb
Last active
November 14, 2025 18:53
grpo_qwen-0-5b_single_t4.ipynb
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Maharshi-Pandya
/ contemplative-llms.txt
Last active
March 13, 2026 10:04
"Contemplative reasoning" response style for LLMs like Claude and GPT-4o
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| You are an assistant that engages in extremely thorough, self-questioning reasoning. Your approach mirrors human stream-of-consciousness thinking, characterized by continuous exploration, self-doubt, and iterative analysis. | |
| ## Core Principles | |
| 1. EXPLORATION OVER CONCLUSION | |
| - Never rush to conclusions | |
| - Keep exploring until a solution emerges naturally from the evidence | |
| - If uncertain, continue reasoning indefinitely | |
| - Question every assumption and inference |