来自实验室的新鲜货

作者:John Knight
Hilbert II (www.qedeq.org)

这是一个令人费解的类别。在这个信息共享和去中心化的时代,共享意识领域又迎来了一个很酷的新成员。Hilbert II 试图复兴并建立在一个近乎夭折的项目 QED 的理想之上(查看末尾的链接以获取 QED 宣言的副本)。Hilbert II 的目标是

...去中心化地访问经过验证且可读的数学知识。正如其名称已经表明的那样,该项目秉承了希尔伯特纲领的传统……Hilbert II 想要成为一个免费的、世界范围内的数学知识库,其中包含形式上正确的数学定理和证明。所有相关文档均根据 GNU 自由文档许可证发布。我们的目标是将常见的数学论证适应形式化的语法。这意味着,每当数学中经常使用某种论证时,我们都会期待将其整合到 Hilbert II 的形式化语言中。这种形式化语言被称为 QEDEQ 格式。

Hilbert II 提供了一个程序套件,使数学家能够将定理和证明放入该知识库中。这些证明由证明检查器自动验证。此外,还可以整合“通用数学语言”的文本。数学公理、定义和命题被组合成所谓的 QEDEQ 模块。这样的模块可以被看作是一本包含形式上正确的证明的数学教科书。由于该系统不是集中管理的,并且可以引用互联网上的任何位置,因此可以构建一个世界范围内的数学知识库。在这个“数学网络”中,任何定理的证明都可以追溯到最基本的规则和公理。想象一下数量惊人的带有超链接的数学教科书,并且其中的每个证明都可以通过 Hilbert II 进行验证。对于每个定理,都可以轻松推导出对其他定理、定义和公理的依赖关系。

Fresh from the Labs

通过 Hilbert II 进行复杂的数学协作世界

安装

首先,Hilbert II 是一个基于 Java 的程序。我们通常尽量避免基于 Java 的项目,因为这里是 Linux Journal,而不是“平台中立的 Java Webstart Journal”,但是更酷的项目绝对值得研究,而且,它确实有一个 Linux 专用版本。对于懒人来说,有一个可以从浏览器启动的 webstart 版本(请参阅本节末尾的链接),这需要您安装 Java 浏览器插件。对于 Linux 版本,工作原型的前提条件是 Java 运行时环境,至少是 1.4 版本。Hilbert II 使用 LaTeX 来实现其许多功能,并且频繁使用的用户可能会遇到一些潜在的错误,因此请查看网站以获取有关可能的 LaTeX 要求的更多信息。

前往网站的下载部分,下载 Linux tarball。将其解压到您选择的目录,并在新的 qedeq 目录中打开终端。

在控制台中,输入

$ ./qedeq_se.sh  

或者,如果这不起作用,请输入

$ sh qedeq_se.sh

用法

Hilbert II 围绕 XML 文件工作,您需要一些 XML 文件才能开始使用。如果您选择“File→Load from web”,则会提供一个默认文件,您可以从中开始实验。如果您查看主窗口,会有一个名为 QEDEQ 的选项卡。单击左侧的任何条目都会在此选项卡中显示其详细信息。在“Tools→LaTeX to QEDEQ”下,您可以开始使用自己的公式,而在“Check→Check Mathematical Logic”下,您可以确保您的语法等检查无误。要导出您的作品供世界查看,请转到“Transform→Create LaTeX output”,这将在 qedeq 下的 generated 文件夹中创建一个新的 LaTeX .tex 文件。

但是从这里开始,您就得靠自己了,因为我对这个高级数学和公式的世界一窍不通(而且在撰写本节的过程中可能说了一些非常不准确的东西)。但是,我渴望看到这种学术合作的成果,理想情况下,知识应该不断进步并不断积累,我希望看到更多这样的令人费解的共享意识项目。

有没有试过在纯文本邮件服务器上工作时,希望有一些像样的游戏来消遣?嗯,您有很多选择,例如冒险文字游戏和 moon-buggy,但我最喜欢的发现是 vitetris,这是一个具有全彩色和多种选项的 俄罗斯方块 克隆。根据 vitetris 网站

vitetris 是 Victor Nilsson 基于终端的 俄罗斯方块 克隆。游戏玩法非常像任天堂早期的 俄罗斯方块 游戏。功能包括

  • 可配置的按键

  • 高分榜

  • 带垃圾的双人模式

  • 网络游戏

  • Linux 上的操纵杆(游戏手柄)支持

它已经在 Linux、Cygwin、NetBSD 和一些其他类 UNIX 系统上进行了测试。库依赖性极小(仅需要 libc),并且可以在编译时禁用许多功能。

Fresh from the Labs

vitetris 提供无需图形的双人 俄罗斯方块 乐趣。

安装

对于那些喜欢二进制文件的人,网站上包含了 RPM 包和一些使用 gcc 3.4.6 为 Slackware 11.0 上的 i486 Linux 构建的 tarball 的链接。但是,vitetris 的依赖性非常少,并且 99% 的人应该能够从源代码 tarball 编译它(从而避免一些不可避免的二进制不兼容性)。实际上,这是我很久以来遇到的最简单、最省心的编译,所以我建议编译它。

从项目网站获取最新的 tarball,解压内容,并在新文件夹中打开终端。进入 vitetris 目录后,输入命令

$ configure
$ make

并且,以 root 或 sudo 身份

# make install

编译完成后,在命令行输入tetris加载游戏。

用法

进入游戏后,您会看到很多很酷的选项。例如,您可以更改您所在关卡的高度,启用顺时针和逆时针方向的旋转,并在游戏模式之间切换。这两种游戏模式启用或禁用攻击其他玩家,方法是用完成的行攻击他们,并将它们添加到对方堆栈的底部(游戏模式 A 用于启用攻击,模式 B 用于禁用攻击)。要独自开始游戏,请选择“1 Player Game”,然后选择您的难度级别和游戏高度即可开始。在您的键盘上,左右箭头键分别向左和向右移动每个方块;向上箭头键旋转屏幕上的方块;向下箭头键进行“软降落”;空格键进行“硬降落”,直接降落到屏幕底部。

如果您想更改按键或在旋转方法等之间切换,您可以在“Options”菜单中进行操作。如果您想玩双人游戏,您还必须在此处定义玩家 2 的按键。如果您在控制台中显示 vitetris 时遇到任何问题,并且想要更改游戏的颜色,甚至切换到单色模式,这些选项也可以在“Options”菜单中找到。

最终,vitetris 本身就是一个很棒的 俄罗斯方块 克隆,但再加上它可以在没有图形界面的命令行上运行,vitetris 是任何系统的绝佳补充,并且在下次 X Window System 无法启动时,它将是一个不错的消遣!

这是我本月遇到的最疯狂的项目!Tetuhi 基本上是一个程序,它接受图像并围绕它生成一个游戏,但它的吸引力不止于此。除了从图像的各个部分制作景观外,Tetuhi 还从图像的其他部分创建角色,以及其他物体,例如食物、弹药、朋友和敌人,所有这些都会在引擎变形原始图像的各个部分时扭动和移动。最重要的是,它还具有动态和自适应的规则集以及不断变化的游戏模式——这意味着每个游戏和图像都可能是真正随机的,并且与上一个不同。

Fresh from the Labs

我意识到这张蜡笔画本身并没有展示 Tetuhi 的功能,但想象一下,山丘和树木在您面前脉动,而您正在驾驶太阳……不,我没有嗑蘑菇!

安装

Tetuhi 绝对是仍在开发中的东西,所以通常的configure && make && make install在这里对您没有多大帮助。在要求方面,您需要最新版本的 Python、GCC、Pygame、Python Imaging Library、PyYAML 和 Gnu Scientific Library。一旦您安装了这些,请前往 Tetuhi 网站,并从 GIT 存储库中获取最新的 tarball 或最新的代码。

一旦您拥有了其中任何一个,解压它(如果您有 tarball),并查看目录 c、img-c 和 perceptron。打开终端,并进入这些目录中的每一个,然后运行命令

$ make

并且,以 root 或 sudo 身份

# make python-install

这应该在所有三个目录中都可以正常工作,没有错误。如果不是,请确保您已安装所有先前提及的库并保持最新。

用法

现在编译已经完成,回到主 tetuhi 目录,并输入命令

$ ./tetuhi nameofimagehere.jpg

如果一切都编译正确,屏幕上应该会出现一个带有疯狂说明的图像,引导您完成游戏的最初步骤。最适合使用的图像类型是那些简洁的图像,例如具有大胆前景元素的鲜明背景。Tetuhi 网页上包含一个 tarball 的链接,其中包含用于测试的示例图像。我最喜欢的是“hills-cars.jpg”,它的陆地、树木和汽车线条都在脉动和回旋,而您控制着一个扭动的太阳——带来了我一段时间以来最迷幻的游戏体验。一旦您享受了最初的几次游戏,您可能想要创建一个指向路径目录的符号链接,这样您就不必一直进入 Tetuhi 的源代码目录。

尽管游戏本身相当简单(并且在大多数情况下都很蹩脚),但真正令人感兴趣的是图像操作的含义。我可以看到代码基础的某些部分在未来会进入游戏和多媒体领域中更大规模的项目。Tetuhi 的创建者 Douglas Bagnall 正在努力使 Tetuhi 能够包含在 One Laptop Per Child XO 笔记本电脑中,因此看看世界各地的孩子们会想出什么样的游戏和图画来与 Tetuhi 的游戏规则结合起来玩,这将是一件很有趣的事情。

查看 Douglas 的其他一些疯狂项目,请访问 halo.gen.nz

项目一览

joyevmouse (welz.org.za/projects/joyevmouse)

joyevmouse 是一个操纵杆到鼠标的映射器,可将操纵杆事件转换为鼠标事件。当然,这意味着像我这样喜欢观看无休止的动漫和 Top Gear 的懒人不必离开沙发了。方便的是,joyevmouse 也完全在用户空间中运行。它不作为内核驱动程序运行,也不需要补丁。目前缺少额外的文档和用户,所以请查看它是否适合您的需求。

Stump Window Manager (Stumpwm, www.nongnu.org/stumpwm)

Stumpwm 是一个键盘驱动的、极简主义的 X11 窗口管理器,用 Common Lisp 编写。尽管其视觉上采用极简主义方法(没有窗口装饰、图标甚至按钮),但 Stumpwm 旨在实现完全可定制且功能非常强大。而且,从其主要功能来看,我会说它是这样的,因为 Stumpwm 旨在在实际程序运行时可破解。终极控制狂会喜欢这一点,任何 Lisp 爱好者也应该看一看。

正在酝酿新鲜、创新或令人费解的东西?请发送电子邮件至 knight.john.a@gmail.com

John Knight 是一位 23 岁的鼓和攀岩狂人,来自世界上最偏远的城市——澳大利亚珀斯。他通常要么埋头于 Audacity 屏幕,要么疯狂地敲击底鼓,直至无法辨认。

加载 Disqus 评论