Systems & Foundations / AIOSS
sokuto
文章生成ゼロで型付き確率決定をミリ秒で返す純Rust推論基盤
LLM特有の遅延肥大化・JSON型破綻・確率過信を根本排除。ModernBERT-jaの単一フォワードパスと置換同変アテンション(SAB)により、CPUのみで12msの確定レイテンシと厳密較正された確率値を両立。
RustModernBERT-jaONNX Runtime+1
[SYS.ID: MI-1222][LOC: TOKYO 35.7°N, 139.7°E][CORE: RUST / GO / TS / LEAN 4][STATUS: 200 OK]
MI-1222
Systems & Cloud Architecture Engineer
terminal — session: active
$ whoami
> MI-1222 | Systems, Cloud & Developer Experience Engineer
$ cat core-focus.txt
> Rust (CST/AST, Systems), Go (Cloud Run, Microservices), TypeScript (DX, Web), Lean 4 (Formal Verification)
課題の本質を見抜き、低レイヤ・基盤からWebまで最適な技術を選び抜く自走型エンジニア。
東京科学大学(旧 東京工業大学)在学。 知的好奇心を原点に、OS・構文解析からクラウドエッジ基盤まで深く探求。 既存ツールの非効率をプロトコルや構文木(CST)のレベルから根本解決します。
# Rust# Go# TypeScript# Lean 4# Cloud Run# Cloudflare
01 //INDEX OF WORKS
Engineering Works
Cloud & Web PlatformsOSS
patto-md
ローカルのMarkdownと添付画像をD&Dで即座にWeb公開するサーバーレス共有基盤
複雑なCMSやログインの壁を排し、手元のMarkdown文書と画像をブラウザへD&Dするだけでパーマリンク発行と即時Web共有を実現。Workers・D1・R2 Presigned PUTの連携により、完全ゼロコスト運用と高速エッジ配信を両立。
Cloudflare WorkersAstroCloudflare R2+1
Productivity & DXOSS
lean4-skills
Mathlib探索・定理証明・エラー診断を自律化するAIエージェント向け形式証明スキル群
AIコーディングエージェントに数学の形式的証明を自律実行させる専用ツールキット。lean --server との対話ゴール取得、7編のエラー処方箋、Loogle型探索を統合し、Python標準ライブラリのみで動作する依存ゼロ設計。
Lean 4MathlibAI Agent+1
Systems & Foundations / AIOSS
LaTeX Beamer Visual Canvas Editor
CSTロスレス同期とGitネイティブなプレゼンエディタ
LaTeX Beamerスライドの視覚的編集とコード直接編集を両立。具象構文木(CST)の双方向同期により、コメントや手動フォーマットを壊さず編集可能。
RustTauri v2LaTeX+1
Systems & Foundations / AIRESEARCH
Theorem Proving & Formalization
Lean 4による数学各種定理・補題の形式化および証明基盤
数学の厳密な論理体系の探求を目的に各種定理をLean 4で形式化。形式的証明の体系的な蓄積を進める個人研究リポジトリ。
Lean 4MathlibProof Search+1
Systems & Foundations / AIPLANNING
Lean 4 Proof Visualizer
定理証明のゴール状態とタクティック適用ツリーを俯瞰する証明可視化システム
形式手法・定理証明系における長大な証明ステップやゴール状態の分岐をグラフィカルに可視化し、証明全体の依存関係と進捗の直感的把握を支援する基盤。
Lean 4AST VisualizationFormal Verification+1
[Planning]
Systems & Foundations / AIPLANNING
bihada
低レイヤ高速画像処理と顔特徴量抽出パイプライン
顔画像の特徴抽出および写真加工を高速かつメモリ安全に行う画像処理パイプライン。Rustによるネイティブ演算エンジンを構築。
RustComputer VisionImage Pipeline
Systems & Foundations / AIRESEARCH
Mojo Language Benchmark & Demo
Mojo言語による並列計算とSIMD最適化の検証リポジトリ
PythonライクなシンタックスとC++並みの性能を持つMojo言語の言語仕様・並列化性能を計測・検証。
MojoSIMDBenchmark+1
Cloud & Web PlatformsOSS
TikZ / LaTeX SVG Rendering API
GCP Cloud Run と Go で実現するミリ秒SVGレンダリング基盤
モバイル端末やWeb環境で重厚なTeXエンジンを直接動かせない制約に対し、GoとCloud Runで最小構成コンテナとエッジキャッシュを統合したミリ秒レイテンシのSVG変換基盤。
GoGCP Cloud RunDocker+1
Cloud & Web PlatformsOSS
Portable TeX Environment (latex_template)
再現性と可搬性を担保したDockerコンテナLaTeXコンパイル環境
OS環境差分による組版崩れを排除するため、最小構成のTeX環境を封入した再現性の高いコンテナ開発環境テンプレート。
DockerTeXLaTeX+1
Cloud & Web PlatformsPLANNING
Interactive Engineering Portfolio (my-portfolio)
自身のことや開発した制作物を視覚的・インタラクティブに紹介する個人サイト
自らの技術的バックボーンや多岐にわたる制作物を、視覚的かつインタラクティブに体験できるポートフォリオサイト。サイバーミニマルな世界観のもと、動的テーマ切り替えや軽快なインタラクションを備える。
AstroTailwind CSS v4Cloudflare Workers+2
Productivity & SecurityOSS
Student Matrix Code Auto-Fill Extension
OSキーチェーン連携により平文保存を完全排除した認証自動化拡張
学生証マトリクスコードの自動入力において、ブラウザへの認証情報平文保存リスクを排除。Chrome拡張のNative Messagingを介してmacOSキーチェーンとセキュアに連携。
TypeScriptChrome MV3Native Messaging+1
Productivity & DXOSS
Obsidian High-Fidelity PDF Exporter
TikZ・Mermaid・数式を忠実にベクターPDF化するObsidianプラグイン
標準PDF出力におけるベクター図や数式のレイアウト崩れを解決。Markdown AST解析と外部SVGレンダラー連携により、モバイル(iOS/Android)でも完全再現する組版プラグイン。
TypeScriptObsidian PluginMarkdown+1
Productivity & DXPLANNING
Markdown Script Studio
非自己回帰推論基盤(System 1)とSingle Sourceデュアル組版を統合した舞台演出台本基盤
自作の非自己回帰推論エンジンにより息継ぎ位置や発話尺をミリ秒でリアルタイム推論。1つのMarkdown/独自DSLから練習用Webアプリと本番用省スペースPDFを完全同期出力。
RustModernBERT-jaTypeScript+3
[Planning]
02 //BACKGROUND & MINDSET
Engineering Journey
[01] ACADEMICS & ROOTS
東工大 × 独学ソフトウェア探求
東京科学大学(旧 東京工業大学)在学。 知的好奇心を原点にRust、Go、TypeScriptを独学で探求し、数学全般(特に圏論や代数学)への関心も深める。 応用情報技術者試験(AP)合格。
[02] PROBLEM-SOLVING
課題に応じた技術選定と実装深度
YAGNI原則に基づき適切な抽象度と技術を選定。 表層の組み合わせにとどまらず、必要であればプロトコルやOS基盤層まで潜り込んで構造的に解決。
[03] ENGINEERING & AUTOMATION
属人性の排除と運用の自動化
型定義やモノレポ構成による安全なコードベースの確立から、各種連携パイプラインの整備まで、 仕組み化によってチームの生産性と堅牢性を向上。