最新

我一直在尝试将不同类型的谜题融合在一起，并重新发明了我称之为“数独单词搜索”的东西。这是一种字母数独谜题，其中单词隐藏在谜题中，你需要推断出单词的位置才能解开谜题。 也就是说，仅凭数独逻辑无法唯一地解开这个谜题。你必须使用两种隐藏单词的逻辑之一来完成谜题：1）推断出单词必须放置的位置并添加字母，或者 2）推断出单词不能放置的位置并限制字母。为了使其更像数独并帮助解题，每一行、每一列和每一个九宫格都至少包含一个已找到单词的字母。 在游戏测试中，我觉得它很有趣，尽管有时对我来说非常困难（我不是数独专家），所以我想把它开发出来分享。 谜题的生成过程是这样的：创建包含 9 个独特字母的字母组，找出所有可以用这些字母组成的单词，生成示例网格，在其中找出单词，剔除不符合单词放置标准的候选谜题，然后通过删除字母来“雕刻”棋盘，直到满足两个条件：数独逻辑的解题方案大于等于 2 个，并且加入单词搜索逻辑后只有 1 个解题方案。总的来说，大约会生成并剔除 60000 个谜题才能得到一个有效的谜题。 我在代码编写过程中广泛使用了 Claude，其中包括： - 谜题生成器 - 谜题解算器 - 谜题解释器 - 静态网站 (Cloudflare) - 在线谜题播放器 (本地存储) - 在线静态谜题 walkthrough - 打印书籍布局 - PDF 布局 总的来说，花几周时间专注于此让我感到非常有趣。 https://www.sudokuwordsearch.com

我认为在像旧手机这样的设备上搭建一个论坛会很有用。目前是否有可用的资源或类似的项目？

您对此有什么经验法则吗？您团队中有人负责这个决定，还是由编写发布版本的人来做决定？

在 Cajal (YC W26)，我们很高兴推出 Talos（[https://github.com/cajal-technologies/talos](https://github.com/cajal-technologies/talos)），这是一个用于在 Lean 中对 WebAssembly 模块进行形式化验证的开源框架。 人工智能现在正在编写大量用于生产的代码。随着代码生成成本的降低，验证成为了瓶颈。我们相信，未来每一段软件都将附带一个数学证明，证明它实现了作者的意图——从而消除许多类型的漏洞。Talos 是实现这一目标的基础之一。 Talos 提供了一个针对二进制级别推理优化的 Wasm 解释器，以及一个用于证明程序属性的最弱前置条件演算层。由于我们直接对 WebAssembly 进行推理，因此任何具有 Wasm 后端的语言都在支持范围内：Rust、C++、Go、C、Swift、Kotlin、Zig、C# 等等。 为了实现这一点，我们使用了 Lean：一种编程语言和定理证明器，它允许您在一个系统中同时编写软件并对其进行数学证明。这使得 Talos 既可以作为可执行解释器，也可以作为 Lean 进行推理的形式化对象。Lean 还集成了现代人工智能证明工具，通过证明搜索和直接评估自动处理目标。 要查看 Talos 的实际应用，请查看对流行的 Rust crate num-integer 中实现的 Stein 的 GCD 算法的证明：[https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588](https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588)。 我们的路线图： - 通过首先通过官方 W3C 测试套件，然后对 SpecTec（形式化 Wasm 规范）进行验证，实现完整的 Wasm 覆盖。 - 任意 crate 验证——任何编译到 Wasm 的 Rust crate 都应在支持范围内。 - 构建我们的证明库 codelib，以使验证日益复杂的程序变得可行。 我们非常希望听到社区对 Talos 的反馈以及对当前形式化验证状态的评论。也欢迎贡献！

工程领导者对用于构建软件的工具缺乏了解。这是同类中首个提供代码仓库级别证据的扫描器。