学ぶオンラインのコースとチュートリアルで Unity の自己学習を進めることができます。学校や大学で創作を学んだり、ユニティを教育カリキュラムに組み込んだりすることができます。プロとしてのスキルセットの幅を広げ、需要の高い仕事に就くための準備を整えましょう。 初心者から上級者まで、Unity学習の旅に必要な情報を見つけてください。
たった200行の純粋なPythonコードだけで構成されGPTの学習と推論を実行できる「MicroGPT」をインタラクティブに解説
MicroGPTは作者のAndrej Karpathy氏によるとLLMをどこまで簡素化できるのかを10年にわたり追求した集大成とのことで、依存関係のない純粋なPythonで書かれた200行の単一ファイルのみであるにもかかわらずGPTに学習と推論を行わせることができます。動作原理についてはAndrej氏のブログで説明されていますが、より初心者向けにスクリプトを用いたインタラクティブな解説を行っているサイトが誕生していたのでどれくらいわかりやすいのか実際に体験してみました。 MicroGPT explained interactively | growingSWE https://growingswe.com/blog/microgpt ◆MicroGPTとはどんなモデルか MicroGPTは3万2000件の人名を通じて統計的パターンを学習し、あたかも実在するかのような人名っぽいものを生成する
Aristotle API
The World's Most Advanced Formal Reasoning Agent> Get access nowWhat others are saying about Aristotle... We’re the #1 formal math model according to ProofBench, by @ValsAI, ahead of the closest competitor by 15%. Aristotle Agent can autonomously prove/formalize for up to 24 hrs without human intervention.
Loogle!
About Loogle searches Lean and Mathlib definitions and theorems. You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot. Usage Loogle finds definitions and lemmas in various ways: By constant: 🔍 Real.sin
Functional Programming in Lean - Functional Programming in Lean
Functional Programming in Lean by David Thrane Christiansen Copyright Microsoft Corporation 2023 This is a free book on using Lean 4 as a programming language. All code samples are tested with Lean 4 release 4.1.0. Release history January, 2024 This is a minor bugfix release that fixes a regression in an example program. October, 2023 In this first maintenance release, a number of smaller issues w
Lean Programming Language
Functional Programming in Lean (FPIL) is the main resource for programmers who want to learn Lean. It assumes a background in programming, but no prior knowledge of functional programming is needed. Theorem Proving in Lean (TPIL) is designed to teach you to develop and verify proofs in Lean and covers dependent type theory, automated proof methods, and Lean-specific features for interactive theore
Theorem Proving in Lean 4
Jeremy AvigadLeonardo de MouraSoonho KongSebastian Ullrich with contributions from the Lean Community This version of the text assumes you’re using Lean 4 (specifically 4.26.0). See the Quickstart section of the Lean documentation to install Lean. The first version of this book was written for Lean 2, and the Lean 3 version is available here.
Theorem Proving in Lean 4 日本語訳 - Theorem Proving in Lean 4 日本語訳
Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community このテキストは読者がLean 4を使うことを前提にしています。Lean 4をインストールするには、Lean 4 Manualの節Quickstartをご覧ください。このテキストの最初のバージョンはLean 2用に書かれました。Lean 3用のバージョンはこちらで入手可能です。 この翻訳について translated by aconite(2章～12章), Haruhisa Enomoto(1章) この翻訳は有志による非公式翻訳です。翻訳に際して、表現を大きく変えた箇所や、分かりやすさを期すため記述やコード例を追加
不確実さを受け入れる — A17Y (1)
ソフトウェア開発に関する認識で大きく変化したもののひとつは不確実性の扱いではなかろうか。古いソフトウェア開発が「複雑さ」を、Agile が「変化」を主要な難しさ、戦うべき敵とみなしたように、今日のソフトウェア開発は「不確実性」との戦いを大きなテーマに据えていると思う。プログラマが不確実性に向ける眼差しは開発プロセスに大小様々な影響を与えている。「達人プログラマー」とその世代は、この変化を捉えていない。 ソフトウェア開発には昔から不確実性がつきものだった。たとえば見積もりでは The Cone of Uncertainty なんて話をする。現代的なソフトウェア開発が昔と違うのは「不確実さは放っておいてもなくならない」ことを認めたことだと思う。The Cone of Uncertainty が象徴する昔のソフトウェア開発では、不確実性は一時的なもので目の前の嵐をやりすごせばいいと考える。極端に
A Formal Verification of Rust's Binary Search Implementation
This post is about my ongoing master’s thesis under Jeremy Avigad at Carnegie Mellon University, in which I’m trying to tackle formal verification of Rust programs in the interactive theorem prover Lean, and a first result of the project: a complete verification of the Rust stdlib’s binary search function. Putting the ‘Formal’ into ‘Formaldehyde’ Formal Verification is the act of mathematically re
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - argumentcomputer/Megaparsec.lean: Lean 4 port of Megaparsec
GitHub - lean-dojo/LeanCopilot: LLMs as Copilots for Theorem Proving in Lean
Moogle: Semantic search over mathlib4
GitHub - 34j/best-of-lean4: A list of awesome lean4 projects. Feel free to add your project.
Learning Lean 4
GitHub - leanprover-community/mathlib4: The math library of Lean 4
GitHub - Kha/electrolysis: Simple verification of Rust programs via functional purification in Lean 2(!)
GitHub - leanprover/theorem_proving_in_lean: Theorem proving in Lean
Lean Web Editor