【形式証明付き】余白に収まるフェルマーの最終定理の証明【AI不使用】
/- Fermat's Last character is T! -/ theorem FLT : "Fermat".toList.getLast! = 't' := rfl これは何？ フェルマーの最終定理、つまり「Fermat(フェルマー)の最終文字はt」の証明です。証明の各ステップは定理証明支援系Leanによって正しさが検証されています。 この記事は何？ 形式的証明があるということは、数学的主張が正しいことを意味しません。何が形式化され、何が証明されたのかを注意深く確認する必要があります。 Leanをはじめとする定理証明支援系を使う際には、数学的主張を定理証明支援系の文法に翻訳（形式化）する必要があります。しかし、定理証明支援系がチェックしてくれるのは「形式化された主張」と「形式化された証明」が噛み合っているかどうかまでで、それが人々が元々意図していた数学的主張と一致しているかどうか
ISUNARABE合同演習2026: AI Agent無制限でチューニングコンテストをやると何が起こるのか見てみたい - Write and Run
KOBA789 です。 忙しい人向けに結論を先に書きます。2026年5月9日（土）に「ISUNARABE合同演習2026」を開催します。つまり ISUCON*1 の模擬大会です。 優勝しても賞金は出ません。あと大事なことですが AI の利用は無制限です。 開催概要 開催日: 2026年5月9日（土） 競技時間: 10:00〜18:00JST チーム人数: 1〜3人（AI 算入せず） 問題: 詳細はポータル公開時に発表します 参考実装の言語: Rust のみ AI の利用: 無制限。ただしベンチマーク中のリクエスト処理に外部リソースを使うことは禁止 参加に必要なもの: AWS アカウント・GitHub アカウント・Discord アカウント 費用: AWS・AI ツールのコストは参加者負担 主催: ISUNARABE（ISUCON 公式とは無関係の非公式イベントです） 賞金は出ません AI
翻訳記事「AIコーディングツールによって加速するコード生成に品質保証活動はどう立ち向かうか」 - ブロッコリーのブログ
はじめに 本記事は、Lilia Abdulina（JetBrains の QA責任者）による研究（Vitaly Sharovatovが協力）である「QA in the Age of AI-Accelerated Development」の翻訳記事です*1*2。 本記事は許諾を得た上で翻訳しています*3。 なお、本記事は現在もGitHub上でディスカッションが続けられています。記事を読んで気になった方や疑問を持った方はぜひディスカッションに参加してください！ 本記事の主な見どころ AIによって「理解の負債」だけでなく、「意図の負債」も増えている AI以前では副産物として獲得できていた「ビジネスドメインの知識」を蓄積できなくなっている 「評価」よりも「予防」に重きを置いている「積極的な品質保証活動を行う企業」と、そうではない「反応的な品質管理を行う企業」が存在する コストはO(n + εn2)
はやく目的のコードに辿り着く
初めてこれがハッカーか、と感じたのは元同僚の @typester だった。 2006年頃、彼の肩越しに覗くと、なにかコードを書いていた。 キーを打つたびに、黒い背景が半分に割れ、テキストのリストが現れ、打鍵のたびにハイライトが移動し絞り込まれていく。 ファイルを飛び回り、一つのファイルに数秒、そしてまた別のファイルへ。 自分もそこそこの秀丸上級者だとは思っていたが、コードベースを駆け抜ける速さに圧倒された。 なぜか画面に反映されるよりもはるかに多くのキーを打っていないか？とは思ったが（Emacs を使っていた :p） 彼をフォローするように Mac を買い、 Emacs を使い始めた。 このエピソードをきっかけに、そしてその後の経験から、 ソフトウェアエンジニアはコードを書くよりもはるかに多くのコードを読むことに時間を割く、 書くはやさだけでなく はやく目的のコードに辿り着くことも重要だと
「難しいのに役に立たない、それが面白い」KOBA789さん ｜私がアウトプットを続ける理由 - Findy Media
Findyスキル偏差値や発信力レベルの上位者に、日々のアウトプットで得られた経験や継続のコツを尋ねる連載企画。今回のゲストは、スキル偏差値「JavaScript 74.2」「Rust 71.7」「TypeScript 71.3」「C++ 66.9」、発信力レベル「9」のKOBA789さんです！ YouTubeチャンネル「#ch789」をVTuberとして運営するKOBA789さんに、技術発信の原点や、現在の発信スタイルを選んだ理由、そしてアウトプットを継続する秘訣を聞きました。 ＞KOBA789さんのポートフォリオを見てみる 制服のまま勉強会へ。中学生で始めたライトニングトーク― はじめにアウトプットを始めたきっかけから教えてください。 中学生の頃に、「クラスメイトと一緒に使う掲示板をつくりたかった」のが大きなきっかけでした。運用するうちに「レスポンスが遅いから、次はチャットをつくりたい」
互換性のある（らしい）DBへの移行など考えるにあたってたいへんざっくり | GREE Engineering
こんにちわ。せじまです。 むかしむかし、社内勉強会で話した内容を公開させていただくということが何度かありました。 TIME_WAITに関する話 EthernetやCPUなどの話 CPUに関する話 先日、社内で「データベースを異なる環境や互換性のあるマネージドサービスなどに移行する際、どういうことを考えてるか、幅広い層に向けて話してください」といった要望がありまして。 久々に話をさせていただきましたので、そのときの資料を公開させていただくことにしました。（いちおう、Speaker DeckにもSlideshareにも両方アップロードしておきました。） 互換性のある（らしい）DBへの移行など考えるにあたってたいへんざっくりfrom Takanori Sejima ※このスライドの内容を全部話すと100〜120分くらいはかかりそうなので、社内ではかいつまんで話しました。 個人的に、データベースの
首都高も郊外も走れる“過去最大の東京”を実現した『Forza Horizon 6』日本マップの全貌――開発陣が明かす熱きこだわりと挑戦【IGN First】
『Forza Horizon 6』の描く日本が、これまでにPlayground Gamesが制作してきた中で最大かつ最も密度の高いマップになることは以前から知られていた。なかでも東京は、チームがこれまでに制作した中で最大の都市空間となり、『Forza Horizon 5』のグアナファトの5倍の広さになる予定であることもわかっていた。 あわせて読みたい日本が舞台の『Forza Horizon 6』約9分の独占ゲームプレイ映像を公開！東京タワーから田園地帯まで、スーパーカーで駆け抜ける――IGN First しかし、それを実際に目にするのはまた別の話で、当然ながら非常に興奮させられる体験だった。私が最初に見たゲームプレイのショーケースでは、本作のカバーカーにも採用された真っ赤な「GR GT」が、マップの南端から北へと進み、東京の郊外を抜け、日本アルプスへ向かって走っていく様子が映し出されていた
Claude Code Skillsのチーム展開で気づいたSkill管理の課題と対策 - 株式会社ヘンリー エンジニアブログ
株式会社ヘンリーでソフトウェアエンジニアをしているwarabiです。 ヘンリーでは以前から開発にClaude Codeを用いていましたが、最近はSkillの活用などでClaude Codeの性能をもっと引き出そうとする動きが活発になっており、ブログでの発信も増えてきています。 Claude Code を活用した電子カルテの外部連携仕様書メンテナンス自動化の取り組み - 株式会社ヘンリー エンジニアブログ 今回は私が以前に作成したSkillをチームの共有物として管理・展開する際に気付いたSkill管理の課題と対策について話そうと思います。 以前作ったSkillの紹介 起票されたIssueの中身を確認・追加調査をしたうえで実装からPR作成までを全自動で行うOrchestrator型のSkillです。（以降 dev Skillと表現） dev.henry.jp このdev Skill作成は元々チ
【解決】チューナー鯖をIntel 省電力モデルに移したらドロップが激しくなった件
あけましておめでとうございます。 先日、テレビを見るための地デジ/BS/CSチューナーを繋いでチューナーサーバーにしていたマシンを、 Core i5-2410Mの半壊ノートPCから、Core i5-9500Tの中古ミニPCに移行しました。 NECのMate MKM22/C-5というモデルです。 中身的にはLenovoのThinkCentre M920q Tinyとほぼ同等品のようです。 ミニPCの稼働時間自体は短いため、半分ぶっ壊れたノートPCよりは保つだろうと思って安心してました。 そしてしっかりテストもせずにEPGStationやらの設定を変えて、年末の紅白とか歌番組の録画予約をバンバンぶち込みました。これが悲劇の始まり。 大晦日、紅白の途中でお風呂に入らなければならず、録画してるし・・・と思ってさっさと入浴して追っかけ再生しようと思ってVLCで開いたら 「終わった。」これしか言葉が出
ブラウザのレイアウトエンジンを自作してみた
前々から自作ブラウザを作ってみたかったんですよね。作ります。 今回はブラウザのGUI周りの、主にレイアウトの座標計算モジュールを自作しました。CSS のボックスモデル, Flex, Grid の座標計算というのが伝わりやすいでしょうか。 HTMLパーサ/CSSパーサ/CSSクエリエンジン/ペインティングも一部実装しましたが、レイアウト可視化のテスト用と割り切っていて、ちゃんと作ったのは主にレイアウトの座標計算周りになります。 作ったもの 雑なプレイグラウンド こんな感じです Terminal で Sixel を描画して Google を表示したもの。今回は主に座標計算周りの実装なので background-color やフォント周りは未実装なんですが、矩形だけでは自分の目視デバッグもしんどかったので、最低限のビットマップフォントをレンダリングできるようにしました。 リポジトリ npm:@m
2025年の振り返り
2025年は色々ありすぎた年だった。人生が進みすぎた。 学業 3月に筑波大学を卒業した。2019年に入学して2回留年して、やっと卒業できた。 自分は昔から本当に勉強ができなくて、高校生の時は大して頭のよくない学校で学年でビリから5番目くらいだったから、6年かかったとはいえ割とまともな大学をちゃんと卒業できたってのは本当に嬉しい。 卒論の出来は本当に悪くて「えっこれでいいの？」ってくらい酷かった。LadybirdブラウザのJavaScript処理系であるLibJSに、可能な限りオーバーヘッドが少なくなるようにGCの動作をトレースするinstrumentationを実装して性能を評価する、みたいなやつをやった。これは実際にはJava向けの既存の手法をほぼそのまま実装しただけのやつなので研究としては普通にめっちゃしょぼかったし、性能評価も「それはそうですよね」という感じだった。 ただ、他の人のや
Google、AI搭載Webブラウザがユーザーの操作から目的を自動で推測、アプリを動的生成して提示する実験的ブラウザ「Disco」を発表
Google、AI搭載Webブラウザがユーザーの操作から目的を自動で推測、アプリを動的生成して提示する実験的ブラウザ「Disco」を発表 旅行の計画を立てようとしてWebブラウザで目的地の観光名所やホテルを何か所も検索していると、Webブラウザがユーザーの意図を理解してAIで自動的にその旅行の計画立案用アプリを動的に生成。新しいタブとしてユーザーに提示することで、ユーザーはたくさんのタブを開いて情報を集めなくてもよくなる。 GoogleでAI関連の実験的製品を開発するGoogle Labsが、そんな新機能を備えた実験的なブラウザ「Disco」を発表しました。 DiscoはGoogleの最新AIモデルであるGeminiを統合したWebブラウザです。 Discoには上記の画面のようにGeminiとチャットする欄があり、ユーザーはGoogleの検索キーワードを入力する代わりに、ここに知りたいこと
Asynchronous Rust on Cortex-M Microcontrollers
In the realm of embedded software, the demand for efficient and responsive applications is ever-increasing. Asynchronous programming, with its ability to handle concurrent tasks effectively, holds immense potential in this domain. Let’s delve into the world of asynchronous Rust specifically tailored for microcontrollers. In this article, we explore the inner workings of Futures, cooperative schedu
オリローで降りる
緩く降りると書いて「緩降機」 屋上に設置されている避難器具、最後は「緩降機」である。家崎さんは「うちの主力製品」だという。 記事の冒頭で見たこちらです。左の箱が屋上に固定されている支柱で、右の箱に器具一式が入っている。 手際よくセッティングする家崎さん。 緩降機のセッティングはこうだ。屋上に固定された支柱を伸ばし、逆L字の形にする。そのL字の先端にあるフックに、「調速機」と呼ばれる機器を取り付ける。 調速機からは長短2本のロープが伸びており、それぞれの端には体に着用するベルトがついている。 家崎さん 井戸のつるべってありますよね？ 水を汲んだ桶を上げると、もう片方の桶が下がる。緩降機も同じ仕組みなんです。ベルトを着けた人間が下に降りると、もう片方の空のベルトが上がってくる。そうやって交互に人を降ろす避難器具なんですよ。 ロープの長さには差があって、長いほうのロープはリールに巻かれている。井
The Blue Envelope #19
Boiler Room関連の話。おれの立場だと関係あると言えばあるし、ないと言えばない。特に結論めいたものはないです はじめに そもそもどういった話かというと、Boiler Room運営のSuperstruct Entertainmentが投資会社KKR Investmentsに買収されたことによって、イスラエルのジェノサイドを含む違法入植や軍需産業に間接的に関与することとなり、我々はどのような態度を取れば良いのかの議論を生んでいる、いった感じである。 個人的には、Boiler Roomに出演することや、イベント自体に遊びに行くことが戦争や差別の肯定にダイレクトにつながるとは考えていない。 親会社であるKKRは巨大なPE投資企業である。当然のようにイスラエル関連企業への投資は過去にあるし、今後もあるであろう。KKRのサイトではその投資ポートフォリオを確認できるが、巨大投資企業であるからそれ
テックブログで「の話」をやめた話 —— 命名のコツもご紹介 - SmartHR Tech Blog
こんにちは、DevRelユニットのinaoです。長らく編集者をやっています。 2年前に部署ができて、それからずっとひとりぼっちなので、そろそろどなたか仲間になってほしいです。 本稿では、「〜の話」というタイトルをSmartHR Tech Blogで基本的にはやめた話と、タイトル命名のコツをご紹介します。 目次 目次 タイトル命名のコツ 記事中のキーワードを使う サブタイトルを積極的に設ける サブタイトルの命名パターン サブタイトルのアンチパターン 「の話」は避ける 見出しの命名もコツは同じ 「の話」をやめるまで 2年前：「の話」の多さに驚くも、静観 1年前：さらに増えてきたので、おそるおそる削減活動を始める 現在：「の話」はこだわりではなかったんだ！ 同じく現在：サブタイトルも浸透 まとめ We Are Hiring! タイトル命名のコツ 「の話」というタイトルをやめたかった理由のご説明も
3ヶ月使ったAIペンダントの比較レビュー：8万円使って結局Plaud AI Note PinからLimitless Pendantに乗り換えた｜高木俊輔 Shunsuke Takagi
追記 2025/10/08 Limitlessペンダントの記事がバズり、紹介リンク経由で世界一Limitlessを売った男になりました。 また、実際の運用のコツなども書いた記事を公開しました この記事では、Plaud AI note pinというAIボイスレコーダーと、Limitless pendantという2つの似たようなガジェットを比較します。筆者は、どちらも購入して最上位のサブスクプランを契約した結果、合計8万円を使いました。 最終的には、聞きなれない人も多いであろう「Limitless Pendant」の方を使い続けて、元々使っていたPlaudは彼女に譲っています。 実際に生活の中で3ヶ月以上毎日使ってみた体験を通して、AIボイスレコーダーについて聞いになっている人の参考になれば幸いです。 お金を使い過ぎてしまったので、もしLimitlessを購入される方は以下のリンクから購入して
ECSのネイティブBlue/Greenが登場したので検証！フック・Dark Canary・コントローラ更新も強力
日本時間2025年7月18日、ECSのデプロイが大幅に強化されたので、試しつつ情報を整理してみました。単純にBlue/Greenがネイティブで可能になっただけではありませんでした。 先に要点 CodeDeployを使わずとも、ネイティブでBlue/Greenデプロイが可能になった lifecycle hooksによって、様々なタイミングでLambdaによる検証も可能 Test listener/listener ruleによって、エンドユーザ影響ゼロで本番環境での事前検証も可能（Dark Canary） Service ConnectでもB/Gが可能に デプロイコントローラをサービス作成後に変更可能に CodeDeployによるB/Gは今後避けた方がよさそう。移行ガイドもあり アップデートの概要 CodeDeployを用いずともECSの組み込み機能としてBlue/Greenデプロイが可能に
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
The Blue Envelope #57
スペースソフト IEEE1394解説 プロトコル